From 3b980d937b5adfbae472ed8a13748a451fdf3450 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 18:17:57 +0200
Subject: Remove calls to global env from indrec

---
 tactics/equality.ml  | 2 +-
 tactics/tacticals.ml | 3 ++-
 tactics/tactics.ml   | 5 +++--
 3 files changed, 6 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 412fbbfd1b..d5fdad0127 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
       match EConstr.kind sigma hdcncl with 
       | Ind (ind_sp,u) -> 
 	let pr1 = 
-	  lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) 
+          lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl)
 	in
         begin match lft2rgt, cls with
         | Some true, None
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ec8d4d0e14..dcd63fe760 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -704,7 +704,8 @@ module New = struct
   (* computing the case/elim combinators *)
 
   let gl_make_elim ind = begin fun gl ->
-    let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
+    let env = Proofview.Goal.env gl in
+    let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in
     let (sigma, c) = pf_apply Evd.fresh_global gl gr in
     (sigma, c)
   end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 206f35c8ba..53a74a5f7d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1455,7 +1455,8 @@ exception IsNonrec
 let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite
 
 let find_ind_eliminator ind s gl =
-  let gr = lookup_eliminator ind s in
+  let env = Proofview.Goal.env gl in
+  let gr = lookup_eliminator env ind s in
   Tacmach.New.pf_apply Evd.fresh_global gl gr
 
 let find_eliminator c gl =
@@ -4128,7 +4129,7 @@ let guess_elim isrec dep s hyp0 gl =
   let sigma, elimc =
     if isrec && not (is_nonrec mind)
     then
-      let gr = lookup_eliminator mind s in
+      let gr = lookup_eliminator env mind s in
       Evd.fresh_global env sigma gr
     else
       let u = EInstance.kind sigma u in
-- 
cgit v1.2.3