Merge PR #11922: No more local reduction functions in Reductionops.

Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares

1 files changed, 14 insertions, 14 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 08178052bf..87b4255b88 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 clenv_unique_resolver ?flags clenv gl =
   let concl = Proofview.Goal.concl gl in
@@ -531,7 +531,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