Remove calls to global env from indrec

plugins/funind/indfun.ml

@@ -382,8 +382,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	let _ =
 	  List.map_i
 	    (fun i x ->
-	     let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
-	     let env = Global.env () in
+              let env = Global.env () in
+              let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in
 	     let evd = ref (Evd.from_env env) in
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 

plugins/ssr/ssrelim.ml

@@ -194,7 +194,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
       let sort = Tacticals.elimination_sort_of_goal gl in
       let gl, elim =
         if not is_case then
-          let t,gl= pf_fresh_global (Indrec.lookup_eliminator (kn,i) sort) gl in
+          let t,gl= pf_fresh_global (Indrec.lookup_eliminator env (kn,i) sort) gl in
           gl, t
         else
           Tacmach.pf_eapply (fun env sigma () ->

plugins/ssr/ssrequality.ml

@@ -340,7 +340,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
   let elim, gl = 
     let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
     let sort = elimination_sort_of_goal gl in
-    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
+    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
     if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
     let elim, _ = destConst elim in
     let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in

pretyping/indrec.ml

@@ -610,11 +610,11 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 (* Look up function for the default elimination constant *)
 
-let lookup_eliminator ind_sp s =
+let lookup_eliminator env ind_sp s =
   let kn,i = ind_sp in
   let mpu = KerName.modpath @@ MutInd.user kn in
   let mpc = KerName.modpath @@ MutInd.canonical kn in
-  let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
+  let ind_id = (lookup_mind kn env).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
   let l = Label.of_id id in
   let knu = KerName.make mpu l in
@@ -623,7 +623,7 @@ let lookup_eliminator ind_sp s =
   (* inductive type *)
   try
     let cst = Constant.make knu knc in
-    let _ = Global.lookup_constant cst in
+    let _ = lookup_constant cst env in
       ConstRef cst
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)

pretyping/indrec.mli

@@ -62,7 +62,7 @@ val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr ->
 
 (** Recursor names utilities *)
 
-val lookup_eliminator : inductive -> Sorts.family -> GlobRef.t
+val lookup_eliminator : env -> inductive -> Sorts.family -> GlobRef.t
 val elimination_suffix : Sorts.family -> string
 val make_elimination_ident : Id.t -> Sorts.family -> Id.t
 

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

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

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