From 69c31d24fc8d058070cc7cadc1df28bfac7f6497 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= <maxime.denes@inria.fr>
Date: Fri, 5 Apr 2019 09:57:49 +0200
Subject: [PATCH] Remove call to global env in pretyping.ml

---
 pretyping/classops.ml  | 10 +++++-----
 pretyping/classops.mli |  2 +-
 pretyping/pretyping.ml |  9 ++++-----
 3 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 20215029afa8..02038190517a 100644
--- a/pretyping/classops.ml
+++ b/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,7 +327,7 @@ 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
@@ -335,7 +335,7 @@ let add_coercion_in_graph env (ic,source,target) =
     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
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 46c6d4c6972e..c04182930e46 100644
--- a/pretyping/classops.mli
+++ b/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 } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a6e3cfe085fa..e29672b6bc19 100644
--- a/pretyping/pretyping.ml
+++ b/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