From 69c31d24fc8d058070cc7cadc1df28bfac7f6497 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 Apr 2019 09:57:49 +0200
Subject: Remove call to global env in pretyping.ml

---
 pretyping/pretyping.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a6e3cfe085..e29672b6bc 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
-- 
cgit v1.2.3


From 5af486406e366bf23558311a7367e573c617e078 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 Apr 2019 12:18:49 +0200
Subject: Remove calls to global env in Inductiveops

---
 pretyping/pretyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e29672b6bc..0f7676cd19 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -644,7 +644,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
 	| None -> []
 	| Some ty ->
           let ((ind, i), u) = destConstruct sigma fj.uj_val in
-	  let npars = inductive_nparams ind in
+          let npars = inductive_nparams !!env ind in
 	    if Int.equal npars 0 then []
 	    else
 	      try
-- 
cgit v1.2.3