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.

5 files changed, 14 insertions, 13 deletions

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