Reductionops.nf_* now take an environment.

6 files changed, 19 insertions, 19 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1207c967b5..311c1c09ec 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1276,7 +1276,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   (* This is a bit too strong I think, in the sense that what we would *)
   (* really like is to have beta-iota reduction only at the positions where *)
   (* parameters are substituted *)
-  let typs = List.map (map_type (nf_betaiota !(pb.evdref))) typs in
+  let typs = List.map (map_type (nf_betaiota pb.env !(pb.evdref))) typs in
 
   (* We build the matrix obtained by expanding the matching on *)
   (* "C x1..xn as x" followed by a residual matching on eqn into *)
@@ -1426,7 +1426,7 @@ and match_current pb (initial,tomatch) =
 	    find_predicate pb.caseloc pb.env pb.evdref
 	      pred current indt (names,dep) tomatch in
 	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
-	  let pred = nf_betaiota !(pb.evdref) pred in
+          let pred = nf_betaiota pb.env !(pb.evdref) pred in
 	  let case =
 	    make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
 	  in
@@ -1663,7 +1663,7 @@ let rec list_assoc_in_triple x = function
 *)
 
 let abstract_tycon ?loc env evdref subst tycon extenv t =
-  let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*)
+  let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*)
   let src = match EConstr.kind !evdref t with
     | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk)
     | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index b646a37f8a..fd83795f55 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -28,8 +28,8 @@ let env_nf_evar sigma env =
 
 let env_nf_betaiotaevar sigma env =
   process_rel_context
-    (fun d e ->
-      push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota sigma c) d) e) env
+    (fun d env ->
+      push_rel (RelDecl.map_constr (fun c -> Reductionops.nf_betaiota env sigma c) d) env) env
 
 (****************************************)
 (* Operations on value/type constraints *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 78de0437d0..1893018a95 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1241,9 +1241,9 @@ let clos_whd_flags flgs env sigma t =
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
 
-let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
-let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
-let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ())
+let nf_beta = clos_norm_flags CClosure.beta
+let nf_betaiota = clos_norm_flags CClosure.betaiota
+let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta
 let nf_all env sigma =
   clos_norm_flags CClosure.all env sigma
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index a277864c92..0565baf45f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -168,9 +168,9 @@ val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
 val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
 
 (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *)
-val nf_beta : local_reduction_function
-val nf_betaiota : local_reduction_function
-val nf_betaiotazeta : local_reduction_function
+val nf_beta : reduction_function
+val nf_betaiota : reduction_function
+val nf_betaiotazeta : reduction_function
 val nf_all : reduction_function
 val nf_evar : evar_map -> constr -> constr
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index f682143f81..9b9408698d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -474,7 +474,7 @@ let contract_fix_use_function env sigma f
   let nbodies = Array.length recindices in
   let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
   let lbodies = List.init nbodies make_Fi in
-  substl_checking_arity env (List.rev lbodies) sigma (nf_beta sigma bodies.(bodynum))
+  substl_checking_arity env (List.rev lbodies) sigma (nf_beta env sigma bodies.(bodynum))
 
 let reduce_fix_use_function env sigma f whfun fix stack =
   match fix_recarg fix (Stack.append_app_list stack Stack.empty) with
@@ -498,7 +498,7 @@ let contract_cofix_use_function env sigma f
   let make_Fi j = (mkCoFix(j,typedbodies), f j) in
   let subbodies = List.init nbodies make_Fi in
   substl_checking_arity env (List.rev subbodies)
-    sigma (nf_beta sigma bodies.(bodynum))
+    sigma (nf_beta env sigma bodies.(bodynum))
 
 let reduce_mind_case_use_function func env sigma mia =
   match EConstr.kind sigma mia.mconstr with
@@ -695,7 +695,7 @@ let rec red_elim_const env sigma ref u largs =
 	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
 	   | NotReducible -> raise Redelimination
-           | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
+           | Reduced (c,rest) -> (nf_beta env sigma c, rest), nocase)
     | EliminationMutualFix (min,refgoal,refinfos) when nargs >= min ->
 	let rec descend (ref,u) args =
 	  let c = reference_value env sigma ref u in
@@ -710,7 +710,7 @@ let rec red_elim_const env sigma ref u largs =
 	let whfun = whd_construct_stack env sigma in
 	(match reduce_fix_use_function env sigma f whfun (destFix sigma d) lrest with
 	   | NotReducible -> raise Redelimination
-	   | Reduced (c,rest) -> (nf_beta sigma c, rest), nocase)
+           | 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
@@ -1101,7 +1101,7 @@ let unfoldoccs env sigma (occs,name) c =
     | [] -> ()
     | _ -> error_invalid_occurrence rest
     in
-    nf_betaiotazeta sigma uc
+    nf_betaiotazeta env sigma uc
   in
   match occs with
     | NoOccurrences -> c
@@ -1282,7 +1282,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	    else raise Not_found
 	  with Not_found ->
           try
-	    let t' = nf_betaiota sigma (one_step_reduce env sigma t) in
+            let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in
             elimrec env t' l
           with NotStepReducible -> error_cannot_recognize ref
   in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8df8f84742..e1720ec955 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -194,7 +194,7 @@ let pose_all_metas_as_evars env evd t =
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
         let ty =
           if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
-          then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
+          then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
           else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
         let src = Evd.evar_source_of_meta mv !evdref in
         let ev = Evarutil.e_new_evar env evdref ~src ty in
@@ -1277,7 +1277,7 @@ let w_coerce env evd mv c =
 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 sigma (nf_meta sigma t) in
+  let t = nf_betaiota env sigma (nf_meta sigma t) in
     unify_0 env sigma CUMUL flags t u
 
 let unify_type env sigma flags mv status c =