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.

16 files changed, 129 insertions, 134 deletions

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