Remove calls to global env in Inductiveops

7 files changed, 83 insertions, 81 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 3ff2e3852d..d9d3764b2a 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -67,17 +67,17 @@ let contradiction_context =
           let id = NamedDecl.get_id d in
           let typ = nf_evar sigma (NamedDecl.get_type d) in
 	  let typ = whd_all env sigma typ in
-	  if is_empty_type sigma typ then
+          if is_empty_type env sigma typ then
 	    simplest_elim (mkVar id)
 	  else match EConstr.kind sigma typ with
-          | Prod (na,t,u) when is_empty_type sigma u ->
-             let is_unit_or_eq = match_with_unit_or_eq_type sigma t in
+          | Prod (na,t,u) when is_empty_type env sigma u ->
+             let is_unit_or_eq = match_with_unit_or_eq_type env sigma t in
              Tacticals.New.tclORELSE
                (match is_unit_or_eq with
                | Some _ ->
                    let hd,args = decompose_app sigma t in
                    let (ind,_ as indu) = destInd sigma hd in
-                   let nparams = Inductiveops.inductive_nparams_env env ind in
+                   let nparams = Inductiveops.inductive_nparams env ind in
                    let params = Util.List.firstn nparams args in
                    let p = applist ((mkConstructUi (indu,1)), params) in
                    (* Checking on the fly that it type-checks *)
@@ -103,7 +103,7 @@ let contradiction_context =
 let is_negation_of env sigma typ t =
   match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (na,t,u) ->
-      is_empty_type sigma u && is_conv_leq env sigma typ t
+      is_empty_type env sigma u && is_conv_leq env sigma typ t
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
@@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) =
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let typ = type_of c in
     let _, ccl = splay_prod env sigma typ in
-    if is_empty_type sigma ccl then
+    if is_empty_type env sigma ccl then
       Tacticals.New.tclTHEN
         (elim false None cl None)
         (Tacticals.New.tclTRY assumption)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 003b069b6e..71ea0098a3 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -81,12 +81,13 @@ let up_to_delta = ref false (* true *)
 let general_decompose recognizer c =
   Proofview.Goal.enter begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
+  let env = pf_env gl in
   let sigma = project gl in
   let typc = type_of c in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
-	    (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma))
+            (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma))
 	      (fun id -> clear [id])));
        exact_no_check c ]
   end
@@ -105,17 +106,17 @@ let head_in indl t gl =
 let decompose_these c l =
   Proofview.Goal.enter begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
-  general_decompose (fun sigma (_,t) -> head_in indl t gl) c
+  general_decompose (fun env sigma (_,t) -> head_in indl t gl) c
   end
 
 let decompose_and c =
   general_decompose
-    (fun sigma (_,t) -> is_record sigma t)
+    (fun env sigma (_,t) -> is_record env sigma t)
     c
 
 let decompose_or c =
   general_decompose
-    (fun sigma (_,t) -> is_disjunction sigma t)
+    (fun env sigma (_,t) -> is_disjunction env sigma t)
     c
 
 let h_decompose l c = decompose_these c l
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d5fdad0127..3d760f1c3d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -446,7 +446,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
     let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in
-      match match_with_equality_type sigma t with
+      match match_with_equality_type env sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
@@ -462,7 +462,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
                   Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
-	          match match_with_equality_type sigma t' with
+                  match match_with_equality_type env sigma t' with
 	            | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
@@ -743,7 +743,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
     let hd2,args2 = whd_all_stack env sigma t2 in
     match (EConstr.kind sigma hd1, EConstr.kind sigma hd2) with
       | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_)
-          when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
+          when Int.equal (List.length args1) (constructor_nallargs env sp1)
             ->
 	  let sorts' =
             Sorts.List.intersect sorts (allowed_sorts env (fst sp1))
@@ -751,7 +751,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
 	  if eq_constructor sp1 sp2 then
-	    let nparams = inductive_nparams_env env ind1 in
+            let nparams = inductive_nparams env ind1 in
 	    let params1,rargs1 = List.chop nparams args1 in
 	    let _,rargs2 = List.chop nparams args2 in
             let (mib,mip) = lookup_mind_specif env ind1 in
@@ -966,9 +966,10 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function
 
 let gen_absurdity id =
   Proofview.Goal.enter begin fun gl ->
+  let env = pf_env gl in
   let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id gl in
-  if is_empty_type sigma hyp_typ
+  if is_empty_type env sigma hyp_typ
   then
     simplest_elim (mkVar id)
   else
@@ -1066,7 +1067,7 @@ let onNegatedEquality with_evars tac =
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     match EConstr.kind sigma (hnf_constr env sigma ccl) with
-    | Prod (_,t,u) when is_empty_type sigma u ->
+    | Prod (_,t,u) when is_empty_type env sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3854606afa..11a8816159 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1355,7 +1355,7 @@ let interp_hints poly =
         let ind = global_inductive_with_alias qid in
 	let mib,_ = Global.lookup_inductive ind in
         Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
-          List.init (nconstructors ind) 
+          List.init (nconstructors env ind)
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
 			empty_hint_info, 
@@ -1391,7 +1391,7 @@ let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
     match EConstr.kind sigma lem with
     | Ind (ind,u) ->
-	List.init (nconstructors ind) 
+        List.init (nconstructors env ind)
 		  (fun i ->
 		   let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd)
 						  (Evd.universe_context_set sigma) in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 08131f6309..e1dad9ad20 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -34,44 +34,42 @@ module RelDecl = Context.Rel.Declaration
 
   -- Eduardo (6/8/97). *)
 
-type 'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option
+type 'a matching_function = Environ.env -> Evd.evar_map -> EConstr.constr -> 'a option
 
-type testing_function  = Evd.evar_map -> EConstr.constr -> bool
+type testing_function  = Environ.env -> Evd.evar_map -> EConstr.constr -> bool
 
 let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
 
-let op2bool = function Some _ -> true | None -> false
-
-let match_with_non_recursive_type sigma t =
+let match_with_non_recursive_type env sigma t =
   match EConstr.kind sigma t with
     | App _ ->
         let (hdapp,args) = decompose_app sigma t in
         (match EConstr.kind sigma hdapp with
            | Ind (ind,u) ->
-               if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then
+               if (Environ.lookup_mind (fst ind) env).mind_finite == CoFinite then
 		 Some (hdapp,args)
 	       else
 		 None
            | _ -> None)
     | _ -> None
 
-let is_non_recursive_type sigma t = op2bool (match_with_non_recursive_type sigma t)
+let is_non_recursive_type env sigma t = Option.has_some (match_with_non_recursive_type env sigma t)
 
 (* Test dependencies *)
 
 (* NB: we consider also the let-in case in the following function,
    since they may appear in types of inductive constructors (see #2629) *)
 
-let rec has_nodep_prod_after n sigma c =
+let rec has_nodep_prod_after n env sigma c =
   match EConstr.kind sigma c with
     | Prod (_,_,b) | LetIn (_,_,_,b) ->
 	( n>0 || Vars.noccurn sigma 1 b)
-	&& (has_nodep_prod_after (n-1) sigma b)
+        && (has_nodep_prod_after (n-1) env sigma b)
     | _            -> true
 
-let has_nodep_prod sigma c = has_nodep_prod_after 0 sigma c
+let has_nodep_prod env sigma c = has_nodep_prod_after 0 env sigma c
 
 (* A general conjunctive type is a non-recursive with-no-indices inductive
    type with only one constructor and no dependencies between argument;
@@ -96,11 +94,11 @@ let rec whd_beta_prod sigma c = match EConstr.kind sigma c with
   | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c)
   | _ -> c
 
-let match_with_one_constructor sigma style onlybinary allow_rec t =
+let match_with_one_constructor env sigma style onlybinary allow_rec t =
   let (hdapp,args) = decompose_app sigma t in
   let res = match EConstr.kind sigma hdapp with
   | Ind ind ->
-      let (mib,mip) = Global.lookup_inductive (fst ind) in
+      let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
       if Int.equal (Array.length mip.mind_consnames) 1
 	&& (allow_rec || not (mis_is_recursive (fst ind,mib,mip)))
         && (Int.equal mip.mind_nrealargs 0)
@@ -125,7 +123,7 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
           let ctyp = whd_beta_prod sigma
             (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in
 	  let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
-	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
+          if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then
 	    (* Record or non strict conjunction *)
 	    Some (hdapp,List.rev cargs)
 	  else
@@ -138,20 +136,20 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
   | Some (hdapp, [_; _]) -> res
   | _ -> None
 
-let match_with_conjunction ?(strict=false) ?(onlybinary=false) sigma t =
-  match_with_one_constructor sigma (Some strict) onlybinary false t
+let match_with_conjunction ?(strict=false) ?(onlybinary=false) env sigma t =
+  match_with_one_constructor env sigma (Some strict) onlybinary false t
 
-let match_with_record sigma t =
-  match_with_one_constructor sigma None false false t
+let match_with_record env sigma t =
+  match_with_one_constructor env sigma None false false t
 
-let is_conjunction ?(strict=false) ?(onlybinary=false) sigma t =
-  op2bool (match_with_conjunction sigma ~strict ~onlybinary t)
+let is_conjunction ?(strict=false) ?(onlybinary=false) env sigma t =
+  Option.has_some (match_with_conjunction env sigma ~strict ~onlybinary t)
 
-let is_record sigma t =
-  op2bool (match_with_record sigma t)
+let is_record env sigma t =
+  Option.has_some (match_with_record env sigma t)
 
-let match_with_tuple sigma t =
-  let t = match_with_one_constructor sigma None false true t in
+let match_with_tuple env sigma t =
+  let t = match_with_one_constructor env sigma None false true t in
   Option.map (fun (hd,l) ->
     let ind = destInd sigma hd in
     let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
@@ -159,8 +157,8 @@ let match_with_tuple sigma t =
     let isrec = mis_is_recursive (fst ind,mib,mip) in
     (hd,l,isrec)) t
 
-let is_tuple sigma t =
-  op2bool (match_with_tuple sigma t)
+let is_tuple env sigma t =
+  Option.has_some (match_with_tuple env sigma t)
 
 (* A general disjunction type is a non-recursive with-no-indices inductive
    type with of which all constructors have a single argument;
@@ -175,11 +173,11 @@ let test_strict_disjunction (mib, mip) =
   in
   Array.for_all_i check 0 mip.mind_nf_lc
 
-let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
+let match_with_disjunction ?(strict=false) ?(onlybinary=false) env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   let res = match EConstr.kind sigma hdapp with
   | Ind (ind,u)  ->
-      let car = constructors_nrealargs ind in
+      let car = constructors_nrealargs env ind in
       let (mib,mip) = Global.lookup_inductive ind in
       if Array.for_all (fun ar -> Int.equal ar 1) car
       && not (mis_is_recursive (ind,mib,mip))
@@ -205,31 +203,31 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
   | Some (hdapp,[_; _]) -> res
   | _ -> None
 
-let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
-  op2bool (match_with_disjunction ~strict ~onlybinary sigma t)
+let is_disjunction ?(strict=false) ?(onlybinary=false) env sigma t =
+  Option.has_some (match_with_disjunction ~strict ~onlybinary env sigma t)
 
 (* An empty type is an inductive type, possible with indices, that has no
    constructors *)
 
-let match_with_empty_type sigma t =
+let match_with_empty_type env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
     | Ind (ind, _) ->
-        let (mib,mip) = Global.lookup_inductive ind in
+        let (mib,mip) = Inductive.lookup_mind_specif env ind in
         let nconstr = Array.length mip.mind_consnames in
 	if Int.equal nconstr 0 then Some hdapp else None
     | _ ->  None
 
-let is_empty_type sigma t = op2bool (match_with_empty_type sigma t)
+let is_empty_type env sigma t = Option.has_some (match_with_empty_type env sigma t)
 
 (* This filters inductive types with one constructor with no arguments;
    Parameters and indices are allowed *)
 
-let match_with_unit_or_eq_type sigma t =
+let match_with_unit_or_eq_type env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
     | Ind (ind , _) ->
-        let (mib,mip) = Global.lookup_inductive ind in
+        let (mib,mip) = Inductive.lookup_mind_specif env ind in
         let nconstr = Array.length mip.mind_consnames in
         if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then
 	  Some hdapp
@@ -237,14 +235,14 @@ let match_with_unit_or_eq_type sigma t =
 	  None
     | _ -> None
 
-let is_unit_or_eq_type sigma t = op2bool (match_with_unit_or_eq_type sigma t)
+let is_unit_or_eq_type env sigma t = Option.has_some (match_with_unit_or_eq_type env sigma t)
 
 (* A unit type is an inductive type with no indices but possibly
    (useless) parameters, and that has no arguments in its unique
    constructor *)
 
-let is_unit_type sigma t =
-  match match_with_conjunction sigma t with
+let is_unit_type env sigma t =
+  match match_with_conjunction env sigma t with
   | Some (_,[]) -> true
   | _ -> false
 
@@ -331,15 +329,16 @@ let match_with_equation env sigma t =
 let is_inductive_equality ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let nconstr = Array.length mip.mind_consnames in
-  Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0
+  let env = Global.env () in
+  Int.equal nconstr 1 && Int.equal (constructor_nrealargs env (ind,1)) 0
 
-let match_with_equality_type sigma t =
+let match_with_equality_type env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args)
   | _ -> None
 
-let is_equality_type sigma t = op2bool (match_with_equality_type sigma t)
+let is_equality_type env sigma t = Option.has_some (match_with_equality_type env sigma t)
 
 (* Arrows/Implication/Negation *)
 
@@ -353,39 +352,39 @@ let match_arrow_pattern env sigma t =
       assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
     | _ -> anomaly (Pp.str "Incorrect pattern matching.")
 
-let match_with_imp_term sigma c =
+let match_with_imp_term env sigma c =
   match EConstr.kind sigma c with
     | Prod (_,a,b) when Vars.noccurn sigma 1 b -> Some (a,b)
     | _              -> None
 
-let is_imp_term sigma c = op2bool (match_with_imp_term sigma c)
+let is_imp_term env sigma c = Option.has_some (match_with_imp_term env sigma c)
 
 let match_with_nottype env sigma t =
   try
     let (arg,mind) = match_arrow_pattern env sigma t in
-    if is_empty_type sigma mind then Some (mind,arg) else None
+    if is_empty_type env sigma mind then Some (mind,arg) else None
   with PatternMatchingFailure -> None
 
-let is_nottype env sigma t = op2bool (match_with_nottype env sigma t)
+let is_nottype env sigma t = Option.has_some (match_with_nottype env sigma t)
 
 (* Forall *)
 
-let match_with_forall_term sigma c=
+let match_with_forall_term env sigma c =
   match EConstr.kind sigma c with
     | Prod (nam,a,b) -> Some (nam,a,b)
     | _            -> None
 
-let is_forall_term sigma c = op2bool (match_with_forall_term sigma c)
+let is_forall_term env sigma c = Option.has_some (match_with_forall_term env sigma c)
 
-let match_with_nodep_ind sigma t =
+let match_with_nodep_ind env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind, _)  ->
-     let (mib,mip) = Global.lookup_inductive ind in
+     let (mib,mip) = Inductive.lookup_mind_specif env ind in
      if Array.length (mib.mind_packets)>1 then None else
        let nodep_constr (ctx, cty) =
         let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
-         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in
+         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) env sigma c in
        if Array.for_all nodep_constr mip.mind_nf_lc then
          let params=
            if Int.equal mip.mind_nrealargs 0 then args else
@@ -395,9 +394,9 @@ let match_with_nodep_ind sigma t =
          None
   | _ -> None
 
-let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t)
+let is_nodep_ind env sigma t = Option.has_some (match_with_nodep_ind env sigma t)
 
-let match_with_sigma_type sigma t =
+let match_with_sigma_type env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind, _) ->
@@ -405,7 +404,7 @@ let match_with_sigma_type sigma t =
      if Int.equal (Array.length (mib.mind_packets)) 1
         && (Int.equal mip.mind_nrealargs 0)
         && (Int.equal (Array.length mip.mind_consnames)1)
-        && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma
+        && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) env sigma
              (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx))
      then
        (*allowing only 1 existential*)
@@ -414,7 +413,7 @@ let match_with_sigma_type sigma t =
        None
   | _ -> None
 
-let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t)
+let is_sigma_type env sigma t = Option.has_some (match_with_sigma_type env sigma t)
 
 (***** Destructing patterns bound to some theory *)
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 741f6713e3..b8c3ddb0f0 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -43,8 +43,8 @@ open Coqlib
    also work on ad-hoc disjunctions introduced by the user.
    (Eduardo, 6/8/97). *)
 
-type 'a matching_function = evar_map -> constr -> 'a option
-type testing_function = evar_map -> constr -> bool
+type 'a matching_function = Environ.env -> evar_map -> constr -> 'a option
+type testing_function = Environ.env -> evar_map -> constr -> bool
 
 val match_with_non_recursive_type : (constr * constr list) matching_function
 val is_non_recursive_type         : testing_function
@@ -83,8 +83,8 @@ val is_inductive_equality  : inductive -> bool
 val match_with_equality_type : (constr * constr list) matching_function
 val is_equality_type       : testing_function
 
-val match_with_nottype     : Environ.env -> (constr * constr) matching_function
-val is_nottype             : Environ.env -> testing_function
+val match_with_nottype     : (constr * constr) matching_function
+val is_nottype             : testing_function
 
 val match_with_forall_term    : (Name.t Context.binder_annot * constr * constr) matching_function
 val is_forall_term            : testing_function
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 53a74a5f7d..066b9c7794 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1432,7 +1432,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
   (general_elim with_evars clear_flag (c,lbindc)
    {elimindex = None; elimbody = (elim,NoBindings);
-    elimrename = Some (false, constructors_nrealdecls (fst mind))})
+    elimrename = Some (false, constructors_nrealdecls env (fst mind))})
   end
 
 let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
@@ -1464,7 +1464,7 @@ let find_eliminator c gl =
   if is_nonrec ind then raise IsNonrec;
   let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
     evd, {elimindex = None; elimbody = (c,NoBindings);
-          elimrename = Some (true, constructors_nrealdecls ind)}
+          elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)}
 
 let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
@@ -1610,9 +1610,9 @@ let descend_in_conjunctions avoid tac (err, info) c =
     let t = Retyping.get_type_of env sigma c in
     let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
     let sign,ccl = EConstr.decompose_prod_assum sigma t in
-    match match_with_tuple sigma ccl with
+    match match_with_tuple env sigma ccl with
     | Some (_,_,isrec) ->
-	let n = (constructors_nrealargs ind).(0) in
+        let n = (constructors_nrealargs env ind).(0) in
 	let sort = Tacticals.New.elimination_sort_of_goal gl in
 	let IndType (indf,_) = find_rectype env sigma ccl in
 	let (_,inst), params = dest_ind_family indf in
@@ -2300,7 +2300,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let whd_all = Tacmach.New.pf_apply whd_all gl in
     let t = whd_all (type_of (mkVar id)) in
-    let eqtac, thin = match match_with_equality_type sigma t with
+    let eqtac, thin = match match_with_equality_type env sigma t with
     | Some (hdcncl,[_;lhs;rhs]) ->
         if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then
           let id' = destVar sigma lhs in
@@ -4740,9 +4740,10 @@ let reflexivity_red allowred =
   (* PL: usual reflexivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+    let env = Tacmach.New.pf_env gl in
     let sigma = Tacmach.New.project gl in
     let concl = maybe_betadeltaiota_concl allowred gl in
-    match match_with_equality_type sigma concl with
+    match match_with_equality_type env sigma concl with
     | None -> Proofview.tclZERO NoEquationFound
     | Some _ -> one_constructor 1 NoBindings
   end