Remove call to global env in pretyping.ml

pretyping/classops.ml

@@ -304,8 +304,8 @@ let install_path_printer f = path_printer := f
 
 let print_path x = !path_printer x
 
-let path_comparator : (inheritance_path -> inheritance_path -> bool) ref =
-  ref (fun _ _ -> false)
+let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref =
+  ref (fun _ _ _ _ -> false)
 
 let install_path_comparator f = path_comparator := f
 
@@ -327,15 +327,15 @@ let different_class_params env i =
       | CL_CONST c -> Environ.is_polymorphic env (ConstRef c)
       | _ -> false
 
-let add_coercion_in_graph env (ic,source,target) =
+let add_coercion_in_graph env sigma (ic,source,target) =
   let old_inheritance_graph = !inheritance_graph in
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
   let try_add_new_path (i,j as ij) p =
     if not (Bijint.Index.equal i j) || different_class_params env i then
       match lookup_path_between_class ij with
       | q ->
-        if not (compare_path p q) then
+        if not (compare_path env sigma p q) then
           ambig_paths := (ij,p)::!ambig_paths;
         false
       | exception Not_found -> (add_new_path ij p; true)
@@ -419,7 +419,7 @@ let declare_coercion env sigma c =
       coe_param = c.coercion_params;
     } in
   let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph env (xf,is,it)
+  add_coercion_in_graph env sigma (xf,is,it)
 
 (* For printing purpose *)
 let pr_cl_index = Bijint.Index.print

pretyping/classops.mli

@@ -111,7 +111,7 @@ val lookup_pattern_path_between :
 val install_path_printer :
   ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
 val install_path_comparator :
-  (inheritance_path -> inheritance_path -> bool) -> unit
+  (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)

pretyping/pretyping.ml

@@ -1146,7 +1146,7 @@ let understand_ltac flags env sigma lvar kind c =
   let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
 
-let path_convertible p q =
+let path_convertible env sigma p q =
   let open Classops in
   let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
   let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
@@ -1171,13 +1171,12 @@ let path_convertible p q =
     | [] -> anomaly (str "A coercion path shouldn't be empty.")
   in
   try
-    let e = Global.env () in
-    let sigma,tp = understand_tcc e (Evd.from_env e) (path_to_gterm p) in
-    let sigma,tq = understand_tcc e sigma (path_to_gterm q) in
+    let sigma,tp = understand_tcc env sigma (path_to_gterm p) in
+    let sigma,tq = understand_tcc env sigma (path_to_gterm q) in
     if Evd.has_undefined sigma then
       false
     else
-      let _ = Evarconv.unify_delay e sigma tp tq in true
+      let _ = Evarconv.unify_delay env sigma tp tq in true
   with Evarconv.UnableToUnify _ | PretypeError _ -> false
 
 let _ = Classops.install_path_comparator path_convertible