No more local reduction functions in Reductionops.

This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.

Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.

42 files changed, 238 insertions, 235 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f82783f47d..a1aac60b35 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -187,7 +187,7 @@ let empty_internalization_env = Id.Map.empty
 
 let compute_internalization_data env sigma id ty typ impl =
   let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in
-  (ty, impl, compute_arguments_scope sigma typ, var_uid id)
+  (ty, impl, compute_arguments_scope env sigma typ, var_uid id)
 
 let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty =
   List.fold_left3
@@ -2358,9 +2358,9 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Id.Set.empty
 
-let scope_of_type_kind sigma = function
+let scope_of_type_kind env sigma = function
   | IsType -> Notation.current_type_scope_name ()
-  | OfType typ -> compute_type_scope sigma typ
+  | OfType typ -> compute_type_scope env sigma typ
   | WithoutTypeConstraint | UnknownIfTermOrType -> None
 
 let allowed_binder_kind_of_type_kind = function
@@ -2377,7 +2377,7 @@ let empty_ltac_sign = {
 let intern_gen kind env sigma
                ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
                c =
-  let tmp_scope = scope_of_type_kind sigma kind in
+  let tmp_scope = scope_of_type_kind env sigma kind in
   let k = allowed_binder_kind_of_type_kind kind in
   internalize env {ids = extract_ids env; unb = false;
                          tmp_scope = tmp_scope; scopes = [];
@@ -2462,7 +2462,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
 
 let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
       { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
-  let tmp_scope = scope_of_type_kind sigma kind in
+  let tmp_scope = scope_of_type_kind env sigma kind in
   let impls = empty_internalization_env in
   let k = allowed_binder_kind_of_type_kind kind in
   internalize env
diff --git a/interp/notation.ml b/interp/notation.ml
index 7761606f11..2703930705 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1448,8 +1448,8 @@ type scope_class = cl_typ
 let scope_class_compare : scope_class -> scope_class -> int =
   cl_typ_ord
 
-let compute_scope_class sigma t =
-  let (cl,_,_) = find_class_type sigma t in
+let compute_scope_class env sigma t =
+  let (cl,_,_) = find_class_type env sigma t in
   cl
 
 module ScopeClassOrd =
@@ -1478,22 +1478,23 @@ let find_scope_class_opt = function
 (**********************************************************************)
 (* Special scopes associated to arguments of a global reference *)
 
-let rec compute_arguments_classes sigma t =
-  match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with
-    | Prod (_,t,u) ->
-        let cl = try Some (compute_scope_class sigma t) with Not_found -> None in
-        cl :: compute_arguments_classes sigma u
+let rec compute_arguments_classes env sigma t =
+  match EConstr.kind sigma (Reductionops.whd_betaiotazeta env sigma t) with
+    | Prod (na, t, u) ->
+        let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (na, t)) env in
+        let cl = try Some (compute_scope_class env sigma t) with Not_found -> None in
+        cl :: compute_arguments_classes env sigma u
     | _ -> []
 
-let compute_arguments_scope_full sigma t =
-  let cls = compute_arguments_classes sigma t in
+let compute_arguments_scope_full env sigma t =
+  let cls = compute_arguments_classes env sigma t in
   let scs = List.map find_scope_class_opt cls in
   scs, cls
 
-let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t)
+let compute_arguments_scope env sigma t = fst (compute_arguments_scope_full env sigma t)
 
-let compute_type_scope sigma t =
-  find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None)
+let compute_type_scope env sigma t =
+  find_scope_class_opt (try Some (compute_scope_class env sigma t) with Not_found -> None)
 
 let current_type_scope_name () =
    find_scope_class_opt (Some CL_SORT)
@@ -1531,15 +1532,16 @@ let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
 let cache_arguments_scope o =
   load_arguments_scope 1 o
 
-let subst_scope_class subst cs =
-  try Some (subst_cl_typ subst cs) with Not_found -> None
+let subst_scope_class env subst cs =
+  try Some (subst_cl_typ env subst cs) with Not_found -> None
 
 let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
   let r' = fst (subst_global subst r) in
   let subst_cl ocl = match ocl with
     | None -> ocl
     | Some cl ->
-        match subst_scope_class subst cl with
+        let env = Global.env () in
+        match subst_scope_class env subst cl with
         | Some cl'  as ocl' when cl' != cl -> ocl'
         | _ -> ocl in
   let cls' = List.Smart.map subst_cl cls in
@@ -1565,7 +1567,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
     | ArgsScopeAuto ->
       let env = Global.env () in (*FIXME?*)
       let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
-      let scs,cls = compute_arguments_scope_full sigma typ in
+      let scs,cls = compute_arguments_scope_full env sigma typ in
       (req,r,List.length scs,scs,cls)
     | ArgsScopeManual ->
       (* Add to the manually given scopes the one found automatically
@@ -1573,7 +1575,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
          of the manually given scopes to avoid further re-computations. *)
       let env = Global.env () in (*FIXME?*)
       let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
-      let l',cls = compute_arguments_scope_full sigma typ in
+      let l',cls = compute_arguments_scope_full env sigma typ in
       let l1 = List.firstn n l' in
       let cls1 = List.firstn n cls in
       (req,r,0,l1@l,cls1)
@@ -1620,7 +1622,7 @@ let find_arguments_scope r =
 let declare_ref_arguments_scope sigma ref =
   let env = Global.env () in (* FIXME? *)
   let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in
-  let (scs,cls as o) = compute_arguments_scope_full sigma typ in
+  let (scs,cls as o) = compute_arguments_scope_full env sigma typ in
   declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
 
 (********************************)
diff --git a/interp/notation.mli b/interp/notation.mli
index 842f2b1458..b427aa9bb3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -264,13 +264,13 @@ type scope_class
 val scope_class_compare : scope_class -> scope_class -> int
 
 val subst_scope_class :
-  Mod_subst.substitution -> scope_class -> scope_class option
+  Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option
 
 val declare_scope_class : scope_name -> scope_class -> unit
 val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit
 
-val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
-val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
+val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option list
+val compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option
 
 (** Get the current scope bound to Sortclass, if it exists *)
 val current_type_scope_name : unit -> scope_name option
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index afc83b780b..0f96b9bbe8 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -259,7 +259,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env sg db j c args =
-  match EConstr.kind sg (whd_betaiotazeta sg c) with
+  match EConstr.kind sg (whd_betaiotazeta env sg c) with
     | App (d, args') ->
         (* We just accumulate the arguments. *)
         extract_type env sg db j d (Array.to_list args' @ args)
@@ -380,7 +380,7 @@ and extract_type_app env sg db (r,s) args =
 and extract_type_scheme env sg db c p =
   if Int.equal p 0 then extract_type env sg db 0 c []
   else
-    let c = whd_betaiotazeta sg c in
+    let c = whd_betaiotazeta env sg c in
     match EConstr.kind sg c with
       | Lambda (n,t,d) ->
           extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 834e4251d3..f13901c36d 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -57,12 +57,12 @@ let make_simple_atoms seq=
       | None->[]
   in {negative=seq.latoms;positive=ratoms}
 
-let do_sequent sigma setref triv id seq i dom atoms=
+let do_sequent env sigma setref triv id seq i dom atoms=
   let flag=ref true in
   let phref=ref triv in
   let do_atoms a1 a2 =
     let do_pair t1 t2 =
-      match unif_atoms sigma i dom t1 t2 with
+      match unif_atoms env sigma i dom t1 t2 with
           None->()
         | Some (Phantom _) ->phref:=true
         | Some c ->flag:=false;setref:=IS.add (c,id) !setref in
@@ -72,16 +72,16 @@ let do_sequent sigma setref triv id seq i dom atoms=
     do_atoms atoms (make_simple_atoms seq);
     !flag && !phref
 
-let match_one_quantified_hyp sigma setref seq lf=
+let match_one_quantified_hyp env sigma setref seq lf=
   match lf.pat with
       Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
-        if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
+        if do_sequent env sigma setref triv lf.id seq i dom lf.atoms then
           setref:=IS.add ((Phantom dom),lf.id) !setref
     | _ -> anomaly (Pp.str "can't happen.")
 
-let give_instances sigma lf seq=
+let give_instances env sigma lf seq=
   let setref=ref IS.empty in
-    List.iter (match_one_quantified_hyp sigma setref seq) lf;
+    List.iter (match_one_quantified_hyp env sigma setref seq) lf;
     IS.elements !setref
 
 (* collector for the engine *)
@@ -129,9 +129,10 @@ let left_instance_tac (inst,id) continue seq=
   let open EConstr in
   Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
+  let env = Proofview.Goal.env gl in
   match inst with
       Phantom dom->
-        if lookup sigma (id,None) seq then
+        if lookup env sigma (id,None) seq then
           tclFAIL 0 (Pp.str "already done")
         else
           tclTHENS (cut dom)
@@ -148,7 +149,7 @@ let left_instance_tac (inst,id) continue seq=
             tclTRY assumption]
     | Real((m,t),_)->
         let c = (m, EConstr.to_constr sigma t) in
-        if lookup sigma (id,Some c) seq then
+        if lookup env sigma (id,Some c) seq then
           tclFAIL 0 (Pp.str "already done")
         else
           let special_generalize=
@@ -205,7 +206,8 @@ let instance_tac inst=
 
 let quantified_tac lf backtrack continue seq =
   Proofview.Goal.enter begin fun gl ->
-  let insts=give_instances (project gl) lf seq in
+  let env = Proofview.Goal.env gl in
+  let insts=give_instances env (project gl) lf seq in
     tclORELSE
       (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
       backtrack
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index c0f4c78ff3..08c2c4d916 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -13,7 +13,7 @@ open Rules
 
 val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t
 
-val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t ->
+val give_instances : Environ.env -> Evd.evar_map -> Formula.t list -> Sequent.t ->
   (Unify.instance * GlobRef.t) list
 
 val quantified_tac : Formula.t list -> seqtac with_backtracking
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7bf13fd25b..3dd5059e5d 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -109,7 +109,7 @@ let deepen seq={seq with depth=seq.depth-1}
 
 let record item seq={seq with history=History.add item seq.history}
 
-let lookup sigma item seq=
+let lookup env sigma item seq=
   History.mem item seq.history ||
   match item with
       (_,None)->false
@@ -117,7 +117,7 @@ let lookup sigma item seq=
         let p (id2,o)=
           match o with
               None -> false
-            | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
+            | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general env sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
           History.exists p seq.history
 
 let add_formula env sigma side nam t seq =
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 3a5da6ad14..bba89c823c 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -39,7 +39,7 @@ val deepen: t -> t
 
 val record: h_item -> t -> t
 
-val lookup: Evd.evar_map -> h_item -> t -> bool
+val lookup: Environ.env -> Evd.evar_map -> h_item -> t -> bool
 
 val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t
 
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index e58e80116d..9c3debe48f 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -29,7 +29,7 @@ let subst_meta subst t =
   let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in
   EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t))
 
-let unif evd t1 t2=
+let unif env evd t1 t2=
   let bige=Queue.create ()
   and sigma=ref [] in
   let bind i t=
@@ -46,8 +46,8 @@ let unif evd t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta evd t1)
-      and nt2=head_reduce (whd_betaiotazeta evd t2) in
+      let nt1=head_reduce (whd_betaiotazeta env evd t1)
+      and nt2=head_reduce (whd_betaiotazeta env evd t2) in
         match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with
             Meta i,Meta j->
               if not (Int.equal i j) then
@@ -123,9 +123,9 @@ let mk_rel_inst evd t=
   in
   let nt=renum_rec 0 t in (!new_rel - 1,nt)
 
-let unif_atoms evd i dom t1 t2=
+let unif_atoms env evd i dom t1 t2=
   try
-    let t=Int.List.assoc i (unif evd t1 t2) in
+    let t=Int.List.assoc i (unif env evd t1 t2) in
       if isMeta evd t then Some (Phantom dom)
       else Some (Real(mk_rel_inst evd t,value evd i t1))
   with
@@ -136,11 +136,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *)
   let l=List.init n (fun i->mkMeta (k+i)) in
     substl l t
 
-let more_general evd (m1,t1) (m2,t2)=
+let more_general env evd (m1,t1) (m2,t2)=
   let mt1=renum_metas_from 0 m1 t1
   and mt2=renum_metas_from m1 m2 t2 in
     try
-      let sigma=unif evd mt1 mt2 in
+      let sigma=unif env evd mt1 mt2 in
       let p (n,t)= n<m1 || isMeta evd t in
         List.for_all p sigma
     with UFAIL(_,_)->false
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 71e786eb90..c6767f04ac 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -13,12 +13,12 @@ open EConstr
 
 exception UFAIL of constr*constr
 
-val unif : Evd.evar_map -> constr -> constr -> (int*constr) list
+val unif : Environ.env -> Evd.evar_map -> constr -> constr -> (int*constr) list
 
 type instance=
     Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
   | Phantom of constr        (* domaine de quantification *)
 
-val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option
+val unif_atoms : Environ.env -> Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option
 
-val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool
+val more_general : Environ.env -> Evd.evar_map -> (int*constr) -> (int*constr) -> bool
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f4200854c2..f0457acd68 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -116,7 +116,7 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) =
         refine to_refine g) ]
 
 let find_rectype env sigma c =
-  let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in
+  let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in
   match EConstr.kind sigma t with
   | Ind ind -> (t, l)
   | Construct _ -> (t, l)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3b8fb48eb0..d6b2a17882 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite."
 
 let rec decompose_app_rel env evd t =
   (* Head normalize for compatibility with the old meta mechanism *)
-  let t = Reductionops.whd_betaiota evd t in
+  let t = Reductionops.whd_betaiota env evd t in
   match EConstr.kind evd t with
   | App (f, [||]) -> assert false
   | App (f, [|arg|]) ->
@@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
     let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
       ~fail:true env sigma in
     let evd = solve_remaining_by env sigma holes by in
-    let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in
+    let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in
     let c1 = nf c1 and c2 = nf c2
     and rew_car = nf car and rel = nf rel
     and prf = nf prf in
@@ -971,7 +971,7 @@ let unfold_match env sigma sk app =
   | App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
       let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
       let v = EConstr.of_constr v in
-        Reductionops.whd_beta sigma (mkApp (v, args))
+        Reductionops.whd_beta env sigma (mkApp (v, args))
   | _ -> app
 
 let is_rew_cast = function RewCast _ -> true | _ -> false
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e05c4c26dd..62d4adca43 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -947,7 +947,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
   let open EConstr in
   if n = 0 then
     let args = List.rev args in
-     (if beta then Reductionops.whd_beta sigma else fun x -> x)
+     (if beta then Reductionops.whd_beta env sigma else fun x -> x)
       (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma
   else match kind_of_type sigma ty with
   | ProdType (_, src, tgt) ->
@@ -1062,11 +1062,12 @@ end
 let introid ?(orig=ref Anonymous) name =
   let open Proofview.Notations in
   Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let g = Proofview.Goal.concl gl in
    match EConstr.kind sigma g with
    | App (hd, _) when EConstr.isLambda sigma hd ->
-      convert_concl_no_check (Reductionops.whd_beta sigma g)
+      convert_concl_no_check (Reductionops.whd_beta env sigma g)
    | _ -> Tacticals.New.tclIDTAC
   end <*>
     (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name))
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ab07dd5be9..29a9c65561 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -281,7 +281,7 @@ let unfoldintac occ rdx t (kt,_) =
           | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
           | Proj _ when same_proj sigma0 c t -> body env t c
           | _ ->
-            let c = Reductionops.whd_betaiotazeta sigma0 c in
+            let c = Reductionops.whd_betaiotazeta env sigma0 c in
             match EConstr.kind sigma0 c with
             | Const _ when EConstr.eq_constr sigma0 c t -> body env t t
             | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
@@ -516,7 +516,7 @@ let rwprocess_rule env dir rule =
     let rec loop d sigma r t0 rs red =
       let t =
         if red = 1 then Tacred.hnf_constr env sigma t0
-        else Reductionops.whd_betaiotazeta sigma t0 in
+        else Reductionops.whd_betaiotazeta env sigma t0 in
       ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t));
       match EConstr.kind sigma t with
       | Prod (_, xt, at) ->
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index adaf7c8cc1..e004613ef3 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -405,7 +405,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
 (* p_origin can be passed to obtain a better error message     *)
 let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
   let k, f, a =
-    let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in
+    let f, a = Reductionops.whd_betaiota_stack env ise (EConstr.of_constr p) in
     let f = EConstr.Unsafe.to_constr f in
     let a = List.map EConstr.Unsafe.to_constr a in
     match kind f with
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fc64022ed4..5e3fb9dae3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1066,7 +1066,7 @@ let adjust_impossible_cases sigma pb pred tomatch submat =
 (*   with .. end                                                             *)
 (*                                                                           *)
 (*****************************************************************************)
-let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
+let specialize_predicate env newtomatchs (names,depna) arsign cs tms ccl =
   (* Assume some gamma st: gamma |- PI [X,x:I(X)]. PI tms. ccl *)
   let nrealargs = List.length names in
   let l = match depna with Anonymous -> 0 | Name _ -> 1 in
@@ -1091,7 +1091,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
   (* We need _parallel_ bindings to get gamma, x1...xn |- PI tms. ccl'' *)
   (* Note: applying the substitution in tms is not important (is it sure?) *)
   let ccl'' =
-    whd_betaiota Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in
+    whd_betaiota env Evd.empty (subst_predicate (realargsi, copti) ccl' tms) in
   (* We adjust ccl st: gamma, x'1..x'n, x1..xn, tms |- ccl'' *)
   let ccl''' = liftn_predicate n (n+1) ccl'' tms in
   (* We finally get gamma,x'1..x'n,x |- [X1;x1:I(X1)]..[Xn;xn:I(Xn)]pred'''*)
@@ -1099,7 +1099,7 @@ let specialize_predicate newtomatchs (names,depna) arsign cs tms ccl =
 
 let find_predicate loc env sigma p current (IndType (indf,realargs)) dep tms =
   let pred = abstract_predicate env sigma indf current realargs dep tms p in
-  (pred, whd_betaiota sigma
+  (pred, whd_betaiota !!env sigma
            (applist (pred, realargs@[current])))
 
 (* Take into account that a type has been discovered to be inductive, leading
@@ -1255,7 +1255,7 @@ let rec generalize_problem names sigma pb = function
       | LocalDef ({binder_name=Anonymous},_,_) -> pb', deps
       | _ ->
          (* for better rendering *)
-        let d = RelDecl.map_type (fun c -> whd_betaiota sigma c) d in
+        let d = RelDecl.map_type (fun c -> whd_betaiota !!(pb.env) sigma c) d in
         let tomatch = lift_tomatch_stack 1 pb'.tomatch in
         let tomatch = relocate_index_tomatch sigma (i+1) 1 tomatch in
         { pb' with
@@ -1352,7 +1352,7 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname)
 
   (* Do the specialization for the predicate *)
   let pred =
-    specialize_predicate typs' (realnames,curname) arsign const_info tomatch pb.pred in
+    specialize_predicate !!(pb.env) typs' (realnames,curname) arsign const_info tomatch pb.pred in
 
   let currents = List.map (fun x -> Pushed (false,x)) typs' in
 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 2a844402a8..f931a32bf8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -108,7 +108,7 @@ let app_opt env sigma f t =
   | None -> sigma, t
   | Some f -> f sigma t
   in
-  sigma, whd_betaiota sigma t
+  sigma, whd_betaiota env sigma t
 
 let pair_of_array a = (a.(0), a.(1))
 
@@ -130,7 +130,7 @@ let disc_subset sigma x =
 exception NoSubtacCoercion
 
 let hnf env sigma c = whd_all env sigma c
-let hnf_nodelta env sigma c = whd_betaiota sigma c
+let hnf_nodelta env sigma c = whd_betaiota env sigma c
 
 let lift_args n sign =
   let rec liftrec k = function
@@ -343,7 +343,7 @@ let app_coercion env sigma coercion v =
   | Some f ->
     let sigma, v' = f sigma v in
     let sigma, v' = Typing.solve_evars env sigma v' in
-    sigma, whd_betaiota sigma v'
+    sigma, whd_betaiota env sigma v'
 
 let coerce_itf ?loc env sigma v t c1 =
   let sigma, coercion = coerce ?loc env sigma t c1 in
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index 49401a9937..0c3eaa1da9 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -164,9 +164,9 @@ let coercion_exists coe = CoeTypMap.mem coe !coercion_tab
 
 (* find_class_type : evar_map -> constr -> cl_typ * universe_list * constr list *)
 
-let find_class_type sigma t =
+let find_class_type env sigma t =
   let open EConstr in
-  let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
+  let t', args = Reductionops.whd_betaiotazeta_stack env sigma t in
   match EConstr.kind sigma t' with
     | Var id -> CL_SECVAR id, EInstance.empty, args
     | Const (sp,u) -> CL_CONST sp, u, args
@@ -178,7 +178,7 @@ let find_class_type sigma t =
     |  _ -> raise Not_found
 
 
-let subst_cl_typ subst ct = match ct with
+let subst_cl_typ env subst ct = match ct with
     CL_SORT
   | CL_FUN
   | CL_SECVAR _ -> ct
@@ -190,7 +190,7 @@ let subst_cl_typ subst ct = match ct with
       if c' == c then ct else (match t with
           | None -> CL_CONST c'
           | Some t ->
-            pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
+            pi1 (find_class_type env Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
   | CL_IND i ->
       let i' = subst_ind subst i in
         if i' == i then ct else CL_IND i'
@@ -204,12 +204,12 @@ let subst_coe_typ subst t = subst_global_reference subst t
 let class_of env sigma t =
   let (t, n1, i, u, args) =
     try
-      let (cl, u, args) = find_class_type sigma t in
+      let (cl, u, args) = find_class_type env sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, u, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
-      let (cl, u, args) = find_class_type sigma t in
+      let (cl, u, args) = find_class_type env sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, u, args)
   in
@@ -217,7 +217,7 @@ let class_of env sigma t =
 
 let inductive_class_of ind = fst (class_info (CL_IND ind))
 
-let class_args_of env sigma c = pi3 (find_class_type sigma c)
+let class_args_of env sigma c = pi3 (find_class_type env sigma c)
 
 let string_of_class = function
   | CL_FUN -> "Funclass"
@@ -249,14 +249,14 @@ let lookup_path_to_sort_from_class s =
 
 let apply_on_class_of env sigma t cont =
   try
-    let (cl,u,args) = find_class_type sigma t in
+    let (cl,u,args) = find_class_type env sigma t in
     let (i, { cl_param = n1 } ) = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
     t, cont i
   with Not_found ->
     (* Is it worth to be more incremental on the delta steps? *)
     let t = Tacred.hnf_constr env sigma t in
-    let (cl, u, args) = find_class_type sigma t in
+    let (cl, u, args) = find_class_type env sigma t in
     let (i, { cl_param = n1 } ) = class_info cl in
     if not (Int.equal (List.length args) n1) then raise Not_found;
     t, cont i
@@ -390,9 +390,10 @@ type coercion = {
 }
 
 let subst_coercion subst c =
+  let env = Global.env () in
   let coe = subst_coe_typ subst c.coercion_type in
-  let cls = subst_cl_typ subst c.coercion_source in
-  let clt = subst_cl_typ subst c.coercion_target in
+  let cls = subst_cl_typ env subst c.coercion_source in
+  let clt = subst_cl_typ env subst c.coercion_target in
   let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
   if c.coercion_type == coe && c.coercion_source == cls &&
      c.coercion_target == clt && c.coercion_is_proj == clp
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index 247ef4df75..31600dd17f 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -26,7 +26,7 @@ type cl_typ =
 (** Equality over [cl_typ] *)
 val cl_typ_eq : cl_typ -> cl_typ -> bool
 
-val subst_cl_typ : substitution -> cl_typ -> cl_typ
+val subst_cl_typ : env -> substitution -> cl_typ -> cl_typ
 
 (** Comparison of [cl_typ] *)
 val cl_typ_ord : cl_typ -> cl_typ -> int
@@ -64,7 +64,7 @@ val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 
 (** [find_class_type env sigma c] returns the head reference of [c],
     its universe instance and its arguments *)
-val find_class_type : evar_map -> types -> cl_typ * EInstance.t * constr list
+val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list
 
 (** raises [Not_found] if not convertible to a class *)
 val class_of : env -> evar_map -> types -> types * cl_index
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index f1506f5f59..36dc01e272 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -136,7 +136,7 @@ let flex_kind_of_term flags env evd c sk =
     | Cast _ | App _ | Case _ -> assert false
 
 let apprec_nohdbeta flags env evd c =
-  let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
+  let (t,sk as appr) = Reductionops.whd_nored_state env evd (c, []) in
   if flags.modulo_betaiota && Stack.not_purely_applicative sk
   then Stack.zip evd (whd_betaiota_deltazeta_for_iota_state
                    flags.open_ts env evd appr)
@@ -496,8 +496,8 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
         let term2 = apprec_nohdbeta flags env evd term2 in
         let default () =
           evar_eqappr_x flags env evd pbty
-            (whd_nored_state evd (term1,Stack.empty))
-            (whd_nored_state evd (term2,Stack.empty))
+            (whd_nored_state env evd (term1,Stack.empty))
+            (whd_nored_state env evd (term2,Stack.empty))
         in
           begin match EConstr.kind evd term1, EConstr.kind evd term2 with
           | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
@@ -556,7 +556,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
       flags.open_ts env' evd (c'1, Stack.empty) in
-    let out2, _ = whd_nored_state evd
+    let out2, _ = whd_nored_state env' evd
       (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty),
       Cst_stack.empty in
     if onleft then evar_eqappr_x flags env' evd CONV out1 out2
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 34684e4a34..348d7c0b2f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -633,7 +633,7 @@ let solve_pattern_eqn env sigma l c =
     l c in
   (* Warning: we may miss some opportunity to eta-reduce more since c'
      is not in normal form *)
-  shrink_eta c'
+  shrink_eta env c'
 
 (*****************************************)
 (* Refining/solving unification problems *)
@@ -1632,7 +1632,7 @@ let rec invert_definition unify flags choose imitate_defs
           map_constr_with_full_binders !evdref (fun d (env,k) -> push_rel d env, k+1)
                                         imitate envk t
   in
-  let rhs = whd_beta evd rhs (* heuristic *) in
+  let rhs = whd_beta env evd rhs (* heuristic *) in
   let fast rhs =
     let filter_ctxt = evar_filtered_context evi in
     let names = ref Id.Set.empty in
@@ -1758,7 +1758,7 @@ let reconsider_unif_constraints unify flags evd =
 let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true)
                      env evd (pbty,(evk1,args1 as ev1),t2) =
   try
-    let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
+    let t2 = whd_betaiota env evd t2 in (* includes whd_evar *)
     let evd = evar_define unify flags ~choose ~imitate_defs env evd pbty ev1 t2 in
       reconsider_unif_constraints unify flags evd
   with
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index b5d81f762a..6132365b27 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -283,9 +283,10 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
         in
         (match optionpos with
            | None ->
+               let env' = push_rel d env in
                mkLambda_name env
-                 (n,t,process_constr (push_rel d env) (i+1)
-                    (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)])))))
+                 (n,t,process_constr env' (i+1)
+                    (EConstr.Unsafe.to_constr (whd_beta env' Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1)])))))
                     (cprest,rest))
            | Some(_,f_0) ->
                let nF = lift (i+1+decF) f_0 in
@@ -293,7 +294,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
                let arg = process_pos env' nF (lift 1 t) in
                mkLambda_name env
                  (n,t,process_constr env' (i+1)
-                    (EConstr.Unsafe.to_constr (whd_beta Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg])))))
+                    (EConstr.Unsafe.to_constr (whd_beta env' Evd.empty (EConstr.of_constr (applist (lift 1 f, [(mkRel 1); arg])))))
                     (cprest,rest)))
     | (LocalDef (n,c,t) as d)::cprest, rest ->
         mkLetIn
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f7e3d651ff..1b6c17fcf9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1025,7 +1025,7 @@ struct
           | [], [] -> []
           | _ -> assert false
         in aux 1 1 (List.rev nal) cs.cs_args, true in
-    let fsign = Context.Rel.map (whd_betaiota sigma) fsign in
+    let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in
     let hypnaming = if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames in
     let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in
     let obj ind rci p v f =
@@ -1134,7 +1134,7 @@ struct
         let pi = lift n pred in (* liftn n 2 pred ? *)
         let pi = beta_applist sigma (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
         let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
-        let cs_args = Context.Rel.map (whd_betaiota sigma) cs_args in
+        let cs_args = Context.Rel.map (whd_betaiota !!env sigma) cs_args in
         let csgn =
           List.map (set_name Anonymous) cs_args
         in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f7456ef35e..4d083664f7 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -603,8 +603,7 @@ end
 (** The type of (machine) states (= lambda-bar-calculus' cuts) *)
 type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> constr -> constr
-type reduction_function = contextual_reduction_function
+type reduction_function = env -> evar_map -> constr -> constr
 type local_reduction_function = evar_map -> constr -> constr
 type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
 
@@ -1225,7 +1224,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
   if tactic_mode then (Stack.best_state sigma s cst_l,Cst_stack.empty) else res
 
 (** reduction machine without global env and refold machinery *)
-let local_whd_state_gen flags sigma =
+let local_whd_state_gen flags _env sigma =
   let rec whrec (x, stack) =
     let c0 = EConstr.kind sigma x in
     let s = (EConstr.of_kind c0, stack) in
@@ -1308,7 +1307,7 @@ let raw_whd_state_gen flags env =
   f
 
 let stack_red_of_state_red f =
-  let f sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f sigma (x, Stack.empty))) in
+  let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in
   f
 
 (* Drops the Cst_stack *)
@@ -1319,8 +1318,8 @@ let iterate_whd_gen refold flags env sigma s =
   Stack.zip sigma ~refold (hd,whd_sk)
   in aux s
 
-let red_of_state_red f sigma x =
-  Stack.zip sigma (f sigma (x,Stack.empty))
+let red_of_state_red f env sigma x =
+  Stack.zip sigma (f env sigma (x,Stack.empty))
 
 (* 0. No Reduction Functions *)
 
@@ -1341,15 +1340,12 @@ let whd_betalet = red_of_state_red whd_betalet_state
 (* 2. Delta Reduction Functions *)
 
 let whd_delta_state e = raw_whd_state_gen CClosure.delta e
-let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
-let whd_delta env = red_of_state_red  (whd_delta_state env)
-
-let whd_betadeltazeta_state e = raw_whd_state_gen CClosure.betadeltazeta e
-let whd_betadeltazeta_stack env =
-  stack_red_of_state_red (whd_betadeltazeta_state env)
-let whd_betadeltazeta env =
-  red_of_state_red (whd_betadeltazeta_state env)
+let whd_delta_stack = stack_red_of_state_red whd_delta_state
+let whd_delta = red_of_state_red whd_delta_state
 
+let whd_betadeltazeta_state = raw_whd_state_gen CClosure.betadeltazeta
+let whd_betadeltazeta_stack = stack_red_of_state_red whd_betadeltazeta_state
+let whd_betadeltazeta = red_of_state_red whd_betadeltazeta_state
 
 (* 3. Iota reduction Functions *)
 
@@ -1361,21 +1357,19 @@ let whd_betaiotazeta_state = local_whd_state_gen CClosure.betaiotazeta
 let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
 let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
 
-let whd_all_state env = raw_whd_state_gen CClosure.all env
-let whd_all_stack env =
-  stack_red_of_state_red (whd_all_state env)
-let whd_all env =
-  red_of_state_red (whd_all_state env)
+let whd_all_state = raw_whd_state_gen CClosure.all
+let whd_all_stack = stack_red_of_state_red whd_all_state
+let whd_all = red_of_state_red whd_all_state
 
-let whd_allnolet_state env = raw_whd_state_gen CClosure.allnolet env
-let whd_allnolet_stack env =
-  stack_red_of_state_red (whd_allnolet_state env)
-let whd_allnolet env =
-  red_of_state_red (whd_allnolet_state env)
+let whd_allnolet_state = raw_whd_state_gen CClosure.allnolet
+let whd_allnolet_stack = stack_red_of_state_red whd_allnolet_state
+let whd_allnolet = red_of_state_red whd_allnolet_state
 
 (* 4. Ad-hoc eta reduction, does not substitute evars *)
 
-let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty))
+let shrink_eta env c =
+  let evd = Evd.from_env env in
+  Stack.zip evd (local_whd_state_gen eta env evd (c,Stack.empty))
 
 (* 5. Zeta Reduction Functions *)
 
@@ -1627,9 +1621,9 @@ let plain_instance sigma s c =
      empty map).
  *)
 
-let instance sigma s c =
+let instance env sigma s c =
   (* if s = [] then c else *)
-  local_strong whd_betaiota sigma (plain_instance sigma s c)
+  strong whd_betaiota env sigma (plain_instance sigma s c)
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -1795,23 +1789,23 @@ let is_arity env sigma c =
 (*************************************)
 (* Metas *)
 
-let meta_value evd mv =
+let meta_value env evd mv =
   let rec valrec mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
       let metas = Metamap.bind valrec b.freemetas in
-      instance evd metas b.rebus
+      instance env evd metas b.rebus
     | None -> mkMeta mv
   in
   valrec mv
 
-let meta_instance sigma b =
+let meta_instance env sigma b =
   let fm = b.freemetas in
   if Metaset.is_empty fm then b.rebus
   else
-    let c_sigma = Metamap.bind (fun mv -> meta_value sigma mv) fm in
-    instance sigma c_sigma b.rebus
+    let c_sigma = Metamap.bind (fun mv -> meta_value env sigma mv) fm in
+    instance env sigma c_sigma b.rebus
 
-let nf_meta sigma c =
+let nf_meta env sigma c =
   let cl = mk_freelisted c in
-  meta_instance sigma { cl with rebus = cl.rebus }
+  meta_instance env sigma { cl with rebus = cl.rebus }
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 243a2745f0..555c4be971 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -127,8 +127,7 @@ end
 
 type state = constr * constr Stack.t
 
-type contextual_reduction_function = env -> evar_map -> constr -> constr
-type reduction_function = contextual_reduction_function
+type reduction_function = env -> evar_map -> constr -> constr
 type local_reduction_function = evar_map -> constr -> constr
 
 type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
@@ -181,30 +180,30 @@ val nf_evar : evar_map -> constr -> constr
 (** Lazy strategy, weak head reduction *)
 
 val whd_evar :  evar_map -> constr -> constr
-val whd_nored : local_reduction_function
-val whd_beta : local_reduction_function
-val whd_betaiota : local_reduction_function
-val whd_betaiotazeta : local_reduction_function
-val whd_all :  contextual_reduction_function
-val whd_allnolet :  contextual_reduction_function
-val whd_betalet : local_reduction_function
+val whd_nored : reduction_function
+val whd_beta : reduction_function
+val whd_betaiota : reduction_function
+val whd_betaiotazeta : reduction_function
+val whd_all :  reduction_function
+val whd_allnolet :  reduction_function
+val whd_betalet : reduction_function
 
 (** Removes cast and put into applicative form *)
-val whd_nored_stack : local_stack_reduction_function
-val whd_beta_stack : local_stack_reduction_function
-val whd_betaiota_stack : local_stack_reduction_function
-val whd_betaiotazeta_stack : local_stack_reduction_function
+val whd_nored_stack : contextual_stack_reduction_function
+val whd_beta_stack : contextual_stack_reduction_function
+val whd_betaiota_stack : contextual_stack_reduction_function
+val whd_betaiotazeta_stack : contextual_stack_reduction_function
 val whd_all_stack : contextual_stack_reduction_function
 val whd_allnolet_stack : contextual_stack_reduction_function
-val whd_betalet_stack : local_stack_reduction_function
+val whd_betalet_stack : contextual_stack_reduction_function
 
-val whd_nored_state : local_state_reduction_function
-val whd_beta_state : local_state_reduction_function
-val whd_betaiota_state : local_state_reduction_function
-val whd_betaiotazeta_state : local_state_reduction_function
+val whd_nored_state : state_reduction_function
+val whd_beta_state : state_reduction_function
+val whd_betaiota_state : state_reduction_function
+val whd_betaiotazeta_state : state_reduction_function
 val whd_all_state : state_reduction_function
 val whd_allnolet_state : state_reduction_function
-val whd_betalet_state : local_state_reduction_function
+val whd_betalet_state : state_reduction_function
 
 (** {6 Head normal forms } *)
 
@@ -214,11 +213,11 @@ val whd_delta :  reduction_function
 val whd_betadeltazeta_stack :  stack_reduction_function
 val whd_betadeltazeta_state :  state_reduction_function
 val whd_betadeltazeta :  reduction_function
-val whd_zeta_stack : local_stack_reduction_function
-val whd_zeta_state : local_state_reduction_function
-val whd_zeta : local_reduction_function
+val whd_zeta_stack : stack_reduction_function
+val whd_zeta_state : state_reduction_function
+val whd_zeta : reduction_function
 
-val shrink_eta : constr -> constr
+val shrink_eta : Environ.env -> constr -> constr
 
 (** Various reduction functions *)
 
@@ -314,5 +313,5 @@ val whd_betaiota_deltazeta_for_iota_state :
   TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
 
 (** {6 Meta-related reduction functions } *)
-val meta_instance : evar_map -> constr freelisted -> constr
-val nf_meta       : evar_map -> constr -> constr
+val meta_instance : env -> evar_map -> constr freelisted -> constr
+val nf_meta       : env -> evar_map -> constr -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 1f091c3df8..5ec5005b3e 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -134,7 +134,7 @@ let retype ?(polyprop=true) sigma =
         let n = inductive_nrealdecls env (fst (fst (dest_ind_family indf))) in
         let t = betazetaevar_applist sigma n p realargs in
         (match EConstr.kind sigma (whd_all env sigma (type_of env t)) with
-          | Prod _ -> whd_beta sigma (applist (t, [c]))
+          | Prod _ -> whd_beta env sigma (applist (t, [c]))
           | _ -> t)
     | Lambda (name,c1,c2) ->
           mkProd (name, c1, type_of (push_rel (LocalAssum (name,c1)) env) c2)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2c717b8774..5b9bc91b84 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -252,7 +252,7 @@ let invert_name labs l {binder_name=na0} env sigma ref na =
                 | None -> None
                 | Some c ->
                     let labs',ccl = decompose_lam sigma c in
-                    let _, l' = whd_betalet_stack sigma ccl in
+                    let _, l' = whd_betalet_stack env sigma ccl in
                     let labs' = List.map snd labs' in
                     (* ppedrot: there used to be generic equality on terms here *)
                     let eq_constr c1 c2 = EConstr.eq_constr sigma c1 c2 in
@@ -288,7 +288,7 @@ let compute_consteval_direct env sigma ref =
 
 let compute_consteval_mutual_fix env sigma ref =
   let rec srec env minarg labs ref c =
-    let c',l = whd_betalet_stack sigma c in
+    let c',l = whd_betalet_stack env sigma c in
     let nargs = List.length l in
     match EConstr.kind sigma c' with
       | Lambda (na,t,g) when List.is_empty l ->
@@ -424,7 +424,7 @@ let solve_arity_problem env sigma fxminargs c =
   let evm = ref sigma in
   let set_fix i = evm := Evd.define i (mkVar vfx) !evm in
   let rec check strict c =
-    let c' = whd_betaiotazeta sigma c in
+    let c' = whd_betaiotazeta env sigma c in
     let (h,rcargs) = decompose_app_vect sigma c' in
     match EConstr.kind sigma h with
         Evar(i,_) when Evar.Map.mem i fxminargs && not (Evd.is_defined !evm i) ->
@@ -725,7 +725,7 @@ let rec red_elim_const env sigma ref u largs =
           if evaluable_reference_eq sigma ref refgoal then
             (c,args)
           else
-            let c', lrest = whd_betalet_stack sigma (applist(c,args)) in
+            let c', lrest = whd_betalet_stack env sigma (applist(c,args)) in
             descend (destEvalRefU sigma c') lrest in
         let (_, midargs as s) = descend (ref,u) largs in
         let d, lrest = whd_nothing_for_iota env sigma (applist s) in
@@ -736,11 +736,11 @@ let rec red_elim_const env sigma ref u largs =
            | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
     | NotAnElimination when unfold_nonelim ->
          let c = reference_value env sigma ref u in
-           (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
+           (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase
     | _ -> raise Redelimination
     with Redelimination when unfold_anyway ->
        let c = reference_value env sigma ref u in
-         (whd_betaiotazeta sigma (applist (c, largs)), []), nocase
+         (whd_betaiotazeta env sigma (applist (c, largs)), []), nocase
 
 and reduce_params env sigma stack l =
   let len = List.length stack in
@@ -849,7 +849,7 @@ and whd_construct_stack env sigma s =
 let try_red_product env sigma c =
   let simpfun c = clos_norm_flags betaiotazeta env sigma c in
   let rec redrec env x =
-    let x = whd_betaiota sigma x in
+    let x = whd_betaiota env sigma x in
     match EConstr.kind sigma x with
       | App (f,l) ->
           (match EConstr.kind sigma f with
@@ -875,7 +875,7 @@ let try_red_product env sigma c =
           | _ -> redrec env c
         in
         let npars = Projection.npars p in
-          (match reduce_projection env sigma p ~npars (whd_betaiotazeta_stack sigma c') [] with
+          (match reduce_projection env sigma p ~npars (whd_betaiotazeta_stack env sigma c') [] with
           | Reduced s -> simpfun (applist s)
           | NotReducible -> raise Redelimination)
       | _ ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index afd6c33821..d1b65775bd 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -179,7 +179,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
       | None -> []
       | Some (rels, ((tc,u), args)) ->
         let instapp =
-          Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
+          Reductionops.whd_beta env sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
         in
         let instapp = EConstr.Unsafe.to_constr instapp in
         let projargs = Array.of_list (args @ [instapp]) in
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 99a35849e0..f0882d4594 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -29,11 +29,11 @@ open Context.Rel.Declaration
 
 module GR = Names.GlobRef
 
-let meta_type evd mv =
+let meta_type env evd mv =
   let ty =
     try Evd.meta_ftype evd mv
     with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
-  meta_instance evd ty
+  meta_instance env evd ty
 
 let inductive_type_knowing_parameters env sigma (ind,u) jl =
   let u = Unsafe.to_instance u in
@@ -175,7 +175,7 @@ let type_case_branches env sigma (ind,largs) pj c =
   let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
   let lc = Array.map EConstr.of_constr lc in
   let n = (snd specif).Declarations.mind_nrealdecls in
-  let ty = whd_betaiota sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
+  let ty = whd_betaiota env sigma (lambda_applist_assum sigma (n+1) p (realargs@[c])) in
   sigma, (lc, ty, Sorts.relevance_of_sort ps)
 
 let judge_of_case env sigma ci pj cj lfj =
@@ -335,7 +335,7 @@ let rec execute env sigma cstr =
   let cstr = whd_evar sigma cstr in
   match EConstr.kind sigma cstr with
     | Meta n ->
-        sigma, { uj_val = cstr; uj_type = meta_type sigma n }
+        sigma, { uj_val = cstr; uj_type = meta_type env sigma n }
 
     | Evar ev ->
         let ty = EConstr.existential_type sigma ev in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 96222f7bf6..5916f0e867 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -35,7 +35,7 @@ val check : env -> evar_map -> constr -> types -> evar_map
 val type_of_variable : env -> variable -> types
 
 (** Returns the instantiated type of a metavariable *)
-val meta_type : evar_map -> metavariable -> types
+val meta_type : env -> evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
 val solve_evars : env -> evar_map -> constr -> evar_map * constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f5aaac315a..ab99bdc777 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -708,8 +708,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
             let stM,stN = extract_instance_status pb in
             let sigma =
               if opt.with_types && flags.check_applied_meta_types then
-                let tyM = Typing.meta_type sigma k1 in
-                let tyN = Typing.meta_type sigma k2 in
+                let tyM = Typing.meta_type curenv sigma k1 in
+                let tyN = Typing.meta_type curenv sigma k2 in
                 let l, r = if k2 < k1 then tyN, tyM else tyM, tyN in
                   check_compatibility curenv CUMUL flags substn l r
               else sigma
@@ -721,7 +721,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
             let sigma =
               if opt.with_types && flags.check_applied_meta_types then
                 (try
-                   let tyM = Typing.meta_type sigma k in
+                   let tyM = Typing.meta_type curenv sigma k in
                    let tyN = get_type_of curenv ~lax:true sigma cN in
                      check_compatibility curenv CUMUL flags substn tyN tyM
                  with RetypeError _ ->
@@ -742,7 +742,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
             if opt.with_types && flags.check_applied_meta_types then
               (try
                  let tyM = get_type_of curenv ~lax:true sigma cM in
-                 let tyN = Typing.meta_type sigma k in
+                 let tyN = Typing.meta_type curenv sigma k in
                    check_compatibility curenv CUMUL flags substn tyM tyN
                with RetypeError _ ->
                  (* Renounce, maybe metas/evars prevents typing *) sigma)
@@ -1040,33 +1040,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
             (match expand_key flags.modulo_delta curenv sigma cf1 with
             | Some c ->
                 unirec_rec curenvnb pb opt substn
-                  (whd_betaiotazeta sigma (mkApp(c,l1))) cN
+                  (whd_betaiotazeta curenv sigma (mkApp(c,l1))) cN
             | None ->
                 (match expand_key flags.modulo_delta curenv sigma cf2 with
                 | Some c ->
                     unirec_rec curenvnb pb opt substn cM
-                      (whd_betaiotazeta sigma (mkApp(c,l2)))
+                      (whd_betaiotazeta curenv sigma (mkApp(c,l2)))
                 | None ->
                     error_cannot_unify curenv sigma (cM,cN)))
         | Some false ->
             (match expand_key flags.modulo_delta curenv sigma cf2 with
             | Some c ->
                 unirec_rec curenvnb pb opt substn cM
-                  (whd_betaiotazeta sigma (mkApp(c,l2)))
+                  (whd_betaiotazeta curenv sigma (mkApp(c,l2)))
             | None ->
                 (match expand_key flags.modulo_delta curenv sigma cf1 with
                 | Some c ->
                     unirec_rec curenvnb pb opt substn
-                      (whd_betaiotazeta sigma (mkApp(c,l1))) cN
+                      (whd_betaiotazeta curenv sigma (mkApp(c,l1))) cN
                 | None ->
                     error_cannot_unify curenv sigma (cM,cN)))
 
   and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
     let f1 () =
       if isApp_or_Proj sigma cM then
-        let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
+        let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in
           if is_open_canonical_projection curenv sigma f1l1 then
-            let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
+            let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in
               solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1080,9 +1080,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
       else
         try f1 () with e when precatchable_exception e ->
           if isApp_or_Proj sigma cN then
-            let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
+            let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in
               if is_open_canonical_projection curenv sigma f2l2 then
-                let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
+                let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in
                   solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
               else error_cannot_unify (fst curenvnb) sigma (cM,cN)
           else error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -1306,18 +1306,18 @@ let w_coerce_to_type env evd c cty mvty =
 
 let w_coerce env evd mv c =
   let cty = get_type_of env evd c in
-  let mvty = Typing.meta_type evd mv in
+  let mvty = Typing.meta_type env evd mv in
   w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env sigma flags c status u =
   let sigma, c = refresh_universes (Some false) env sigma c in
-  let t = get_type_of env sigma (nf_meta sigma c) in
-  let t = nf_betaiota env sigma (nf_meta sigma t) in
+  let t = get_type_of env sigma (nf_meta env sigma c) in
+  let t = nf_betaiota env sigma (nf_meta env sigma t) in
     unify_0 env sigma CUMUL flags t u
 
 let unify_type env sigma flags mv status c =
-  let mvty = Typing.meta_type sigma mv in
-  let mvty = nf_meta sigma mvty in
+  let mvty = Typing.meta_type env sigma mv in
+  let mvty = nf_meta env sigma mvty in
     unify_to_type env sigma
       (set_flags_for_type flags)
       c status mvty
@@ -1476,20 +1476,20 @@ let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
    [clenv_typed_unify M N clenv] expects in addition that expected
    types of metavars are unifiable with the types of their instances    *)
 
-let head_app sigma m =
-  fst (whd_nored_state sigma (m, Stack.empty))
+let head_app env sigma m =
+  fst (whd_nored_state env sigma (m, Stack.empty))
 
 let isEvar_or_Meta sigma c = match EConstr.kind sigma c with
 | Evar _ | Meta _ -> true
 | _ -> false
 
 let check_types env flags (sigma,_,_ as subst) m n =
-  if isEvar_or_Meta sigma (head_app sigma m) then
+  if isEvar_or_Meta sigma (head_app env sigma m) then
     unify_0_with_initial_metas subst true env CUMUL
       flags
       (get_type_of env sigma n)
       (get_type_of env sigma m)
-  else if isEvar_or_Meta sigma (head_app sigma n) then
+  else if isEvar_or_Meta sigma (head_app env sigma n) then
     unify_0_with_initial_metas subst true env CUMUL
       flags
       (get_type_of env sigma m)
@@ -1947,7 +1947,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
   (* Remove delta when looking for a subterm *)
   let flags = { flags with core_unify_flags = flags.subterm_unify_flags } in
   let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
-  let typp = Typing.meta_type evd' p in
+  let typp = Typing.meta_type env evd' p in
   let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
   match infer_conv ~pb:CUMUL env evd' predtyp typp with
   | None ->
@@ -1958,7 +1958,7 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
           (evd',[p,pred,(Conv,TypeProcessed)],[])
 
 let secondOrderDependentAbstraction env evd flags typ (p, oplist) =
-  let typp = Typing.meta_type evd p in
+  let typp = Typing.meta_type env evd p in
   let evd, pred = abstract_list_all_with_dependencies env evd typp typ oplist in
   w_merge env false flags.merge_unify_flags
           (evd,[p,pred,(Conv,TypeProcessed)],[])
@@ -1968,8 +1968,8 @@ let secondOrderAbstractionAlgo dep =
   if dep then secondOrderDependentAbstraction else secondOrderAbstraction
 
 let w_unify2 env evd flags dep cv_pb ty1 ty2 =
-  let c1, oplist1 = whd_nored_stack evd ty1 in
-  let c2, oplist2 = whd_nored_stack evd ty2 in
+  let c1, oplist1 = whd_nored_stack env evd ty1 in
+  let c2, oplist2 = whd_nored_stack env evd ty2 in
   match EConstr.kind evd c1, EConstr.kind evd c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
@@ -2000,8 +2000,8 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
    convertible and first-order otherwise. But if failed if e.g. the type of
    Meta(1) had meta-variables in it. *)
 let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
-  let hd1,l1 = decompose_app_vect evd (whd_nored evd ty1) in
-  let hd2,l2 = decompose_app_vect evd (whd_nored evd ty2) in
+  let hd1,l1 = decompose_app_vect evd (whd_nored env evd ty1) in
+  let hd2,l2 = decompose_app_vect evd (whd_nored env evd ty2) in
   let is_empty1 = Array.is_empty l1 in
   let is_empty2 = Array.is_empty l2 in
     match EConstr.kind evd hd1, not is_empty1, EConstr.kind evd hd2, not is_empty2 with
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 37d54a4eea..2f0e472095 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -41,11 +41,11 @@ type clausenv = {
 let cl_env ce = ce.env
 let cl_sigma ce =  ce.evd
 
-let clenv_nf_meta clenv c = nf_meta clenv.evd c
-let clenv_term clenv c = meta_instance clenv.evd c
-let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
-let clenv_value clenv = meta_instance clenv.evd clenv.templval
-let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
+let clenv_nf_meta clenv c = nf_meta clenv.env clenv.evd c
+let clenv_term clenv c = meta_instance clenv.env clenv.evd c
+let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv
+let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval
+let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp
 
 let refresh_undefined_univs clenv =
   match EConstr.kind clenv.evd clenv.templval.rebus with
@@ -212,19 +212,19 @@ let clenv_assign mv rhs clenv =
    In any case, we respect the order given in A.
 *)
 
-let clenv_metas_in_type_of_meta evd mv =
-  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
+let clenv_metas_in_type_of_meta env evd mv =
+  (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas
 
 let dependent_in_type_of_metas clenv mvs =
   List.fold_right
-    (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.evd mv))
+    (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.env clenv.evd mv))
     mvs Metaset.empty
 
 let dependent_closure clenv mvs =
   let rec aux mvs acc =
     Metaset.fold
       (fun mv deps ->
-        let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in
+        let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.env clenv.evd mv in
         aux metas_of_meta_type (Metaset.union deps metas_of_meta_type))
       mvs acc in
   aux mvs mvs
@@ -251,7 +251,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce
 
 (* Instantiate metas that create beta/iota redexes *)
 
-let meta_reducible_instance evd b =
+let meta_reducible_instance env evd b =
   let fm = b.freemetas in
   let fold mv accu =
     let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in
@@ -261,7 +261,7 @@ let meta_reducible_instance evd b =
   in
   let metas = Metaset.fold fold fm Metamap.empty in
   let rec irec u =
-    let u = whd_betaiota Evd.empty u (* FIXME *) in
+    let u = whd_betaiota env Evd.empty u (* FIXME *) in
     match EConstr.kind evd u with
     | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
         let m = destMeta evd (strip_outer_cast evd c) in
@@ -314,12 +314,12 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
 let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl =
-  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd clenv.templtyp.rebus))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
   else
     clenv_unify CUMUL ~flags
-      (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
+      (meta_reducible_instance clenv.env clenv.evd clenv.templtyp) concl clenv
 
 let old_clenv_unique_resolver ?flags clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
@@ -535,7 +535,7 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then
+  if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 695e103082..6f24310cdb 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -36,7 +36,7 @@ let clenv_cast_meta clenv =
     match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with
       | Meta mv ->
           (try
-            let b = Typing.meta_type clenv.evd mv in
+            let b = Typing.meta_type clenv.env clenv.evd mv in
             assert (not (occur_meta clenv.evd b));
             if occur_meta clenv.evd b then u
             else mkCast (mkMeta mv, DEFAULTcast, b)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 28b5ed5811..7b323ee0ed 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -485,7 +485,7 @@ let unfold_head env sigma (ids, csts) c =
         true, EConstr.of_constr (Environ.constant_value_in env (cst, u))
     | App (f, args) ->
         (match aux f with
-        | true, f' -> true, Reductionops.whd_betaiota sigma (mkApp (f', args))
+        | true, f' -> true, Reductionops.whd_betaiota env sigma (mkApp (f', args))
         | false, _ ->
             let done_, args' =
               Array.fold_left_i (fun i (done_, acc) arg ->
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 7c702eab3a..6da2248cc3 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -653,7 +653,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
         (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p)
           (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp)
             (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind)
-              (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma
+              (EConstr.Unsafe.to_constr (Reductionops.whd_beta env sigma
                 (EConstr.of_constr (applist (c,
                   Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))))
       in c', ctx'
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e1d34af13e..31384a353c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -423,7 +423,8 @@ let type_of_clause cls gl = match cls with
 let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
   Proofview.Goal.enter begin fun gl ->
   let evd = Proofview.Goal.sigma gl in
-  let isatomic = isProd evd (whd_zeta evd hdcncl) in
+  let env = Proofview.Goal.env gl in
+  let isatomic = isProd evd (whd_zeta env evd hdcncl) in
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun evd c type_of_cls in
@@ -458,7 +459,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let sigma = Tacmach.New.project gl in
       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
+    let rels, t = decompose_prod_assum sigma (whd_betaiotazeta env sigma ctype) in
       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
@@ -475,7 +476,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 env 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
@@ -1214,7 +1215,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with Evarconv.UnableToUnify _ ->
         user_err Pp.(str "Cannot solve a unification problem.")
     else
-      let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with
+      let (a,p_i_minus_1) = match whd_beta_stack env sigma p_i with
         | (_sigS,[a;p]) -> (a, p)
         | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
       let sigma, ev = Evarutil.new_evar env sigma a in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 76b1c94759..5338e0eef5 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -88,9 +88,9 @@ let is_lax_conjunction = function
 let prod_assum sigma t = fst (decompose_prod_assum sigma t)
 
 (* whd_beta normalize the types of arguments in a product *)
-let rec whd_beta_prod sigma c = match EConstr.kind sigma c with
-  | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta sigma t,whd_beta_prod sigma c)
-  | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c)
+let rec whd_beta_prod env sigma c = match EConstr.kind sigma c with
+  | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta env sigma t,whd_beta_prod env sigma c)
+  | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod env sigma c)
   | _ -> c
 
 let match_with_one_constructor env sigma style onlybinary allow_rec t =
@@ -119,7 +119,7 @@ let match_with_one_constructor env sigma style onlybinary allow_rec t =
         else
           let ctx, cty = mip.mind_nf_lc.(0) in
           let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
-          let ctyp = whd_beta_prod sigma
+          let ctyp = whd_beta_prod env 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 env sigma ctyp then
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4809332c5..d0a13a8a40 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1319,7 +1319,7 @@ let cut c =
       let r = Sorts.relevance_of_sort s in
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in
       (* Backward compat: normalize [c]. *)
-      let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
+      let c = if normalize_cut then strong whd_betaiota env sigma c else c in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
         (Refine.refine ~typecheck:false begin fun h ->
             let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in
@@ -1607,7 +1607,7 @@ let make_projection env sigma params cstr sign elim i n c u =
         noccur_between sigma 1 (n-i-1) t
         (* to avoid surprising unifications, excludes flexible
         projection types or lambda which will be instantiated by Meta/Evar *)
-        && not (isEvar sigma (fst (whd_betaiota_stack sigma t)))
+        && not (isEvar sigma (fst (whd_betaiota_stack env sigma t)))
         && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t))
       then
         let t = lift (i+1-n) t in
@@ -3025,7 +3025,7 @@ let specialize (c,lbind) ipat =
       let flags = { (default_unify_flags ()) with resolve_evars = true } in
       let clause = clenv_unify_meta_types ~flags clause in
       let sigma = clause.evd in
-      let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in
+      let (thd,tstack) = whd_nored_stack env sigma (clenv_value clause) in
       (* The completely applied term is (thd tstack), but tstack may
          contain unsolved metas, so now we must reabstract them
          args with there name to have
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 743d1d2026..5323c9f1c6 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -139,7 +139,7 @@ let build_beq_scheme_deps kn =
        perfomed in a much cleaner way, e.g. using the kernel normal form of
        constructor types and kernel whd_all for the argument types. *)
     let rec aux accu c =
-      let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+      let (c,a) = Reductionops.whd_betaiota_stack env Evd.empty EConstr.(of_constr c) in
       let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
       match Constr.kind c with
       | Cast (x,_,_) -> aux accu (Term.applist (x,a))
@@ -238,7 +238,7 @@ let build_beq_scheme mode kn =
     let compute_A_equality rel_list nlist eqA ndx t =
       let lifti = ndx in
       let rec aux c =
-        let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+        let (c,a) = Reductionops.whd_betaiota_stack env Evd.empty EConstr.(of_constr c) in
         let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
         match Constr.kind c with
         | Rel x -> mkRel (x-nlist+ndx)
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index d6be02245c..3cc5dd65af 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -111,7 +111,7 @@ la liste des variables dont depend la classe source
 l'indice de la classe source dans la liste lp
 *)
 
-let get_source lp source =
+let get_source env lp source =
   let open Context.Rel.Declaration in
   match source with
     | None ->
@@ -120,7 +120,7 @@ let get_source lp source =
          | [] -> raise Not_found
          | LocalDef _ :: lt -> aux lt
          | LocalAssum (_,t1) :: lt ->
-            let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in
+            let cl1,u1,lv1 = find_class_type env Evd.empty (EConstr.of_constr t1) in
             cl1,lt,lv1,1
        in aux lp
     | Some cl ->
@@ -130,17 +130,17 @@ let get_source lp source =
          | LocalDef _ as decl :: lt -> aux (decl::acc) lt
          | LocalAssum (_,t1) as decl :: lt ->
             try
-              let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in
+              let cl1,u1,lv1 = find_class_type env Evd.empty (EConstr.of_constr t1) in
               if cl_typ_eq cl cl1 then cl1,acc,lv1,Context.Rel.nhyps lt+1
               else raise Not_found
             with Not_found -> aux (decl::acc) lt
        in aux [] (List.rev lp)
 
-let get_target t ind =
+let get_target env t ind =
   if (ind > 1) then
     CL_FUN
   else
-    match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
+    match pi1 (find_class_type env Evd.empty (EConstr.of_constr t)) with
     | CL_CONST p when Recordops.is_primitive_projection p ->
       CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
     | x -> x
@@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly =
     match idf_opt with
       | Some idf -> idf
       | None ->
-          let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in
+          let cl,u,_ = find_class_type env sigma (EConstr.of_constr t) in
           Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
@@ -298,14 +298,15 @@ let warn_uniform_inheritance =
 
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
-  let t, _ = Typeops.type_of_global_in_context (Global.env ()) coef in
+  let env = Global.env () in
+  let t, _ = Typeops.type_of_global_in_context env coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let lp,tg = decompose_prod_assum t in
   let llp = List.length lp in
   if Int.equal llp 0 then raise (CoercionError NotAFunction);
   let (cls,ctx,lvs,ind) =
     try
-      get_source lp source
+      get_source env lp source
     with Not_found ->
       raise (CoercionError (NoSource source))
   in
@@ -315,7 +316,7 @@ let add_new_coercion_core coef stre poly source target isid =
     warn_uniform_inheritance coef;
   let clt =
     try
-      get_target tg ind
+      get_target env tg ind
     with Not_found ->
       raise (CoercionError NoTarget)
   in
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 2fd6fe2b29..ec37ec7fa8 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -33,7 +33,7 @@ let project_hint ~poly pri l2r r =
   let p = if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
   let sigma, p = Evd.fresh_global env sigma p in
   let c =
-    Reductionops.whd_beta sigma
+    Reductionops.whd_beta env sigma
       (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign))
   in
   let c =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3b9c771b93..53f3c8408b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1755,7 +1755,8 @@ let cache_scope_command o =
 
 let subst_scope_command (subst,(local,scope,o as x)) = match o with
   | ScopeClasses cl ->
-      let cl' = List.map_filter (subst_scope_class subst) cl in
+      let env = Global.env () in
+      let cl' = List.map_filter (subst_scope_class env subst) cl in
       let cl' =
         if List.for_all2eq (==) cl cl' then cl
         else cl' in