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.

2 files changed, 15 insertions, 15 deletions

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)