3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a5c19f3217..e582362e25 100644
--- a/plugins/funind/indfun.ml
+++ b/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 
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 350bb9019e..675e4d2457 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/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 () ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 5abbc214de..a7a3fee942 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/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