Fix some warnings

compiler/shared_ast/var.ml

@@ -56,6 +56,7 @@ module Generic = struct
   let t v = Var v
   let get (Var v) = Bindlib.copy_var v (fun x -> EVar x) (Bindlib.name_of v)
   let compare (Var x) (Var y) = Bindlib.compare_vars x y
+  let eq (Var x) (Var y) = Bindlib.eq_vars x y [@@ocaml.warning "-32"]
 end
 
 (* Wrapper around Set.Make to re-add type parameters (avoid inconsistent

compiler/shared_ast/var.mli

@@ -23,6 +23,7 @@ open Types
 
 type 'e t = 'e Bindlib.var constraint 'e = ([< any ], 't) gexpr
 type 'e vars = 'e Bindlib.mvar
+type 'e binder = ('e, 'e marked) Bindlib.binder
 
 val make : string -> 'e t
 val compare : 'e t -> 'e t -> int

compiler/verification/io.mli

@@ -17,7 +17,6 @@
 
 (** Common code for handling the IO of all proof backends supported *)
 
-open Utils
 open Shared_ast
 
 module type Backend = sig

compiler/verification/solver.ml

@@ -14,8 +14,6 @@
    License for the specific language governing permissions and limitations under
    the License. *)
 
-open Dcalc.Ast
-
 (** [solve_vc] is the main entry point of this module. It takes a list of
     expressions [vcs] corresponding to verification conditions that must be
     discharged by Z3, and attempts to solve them **)