Reductionops.nf_* now take an environment.

17 files changed, 57 insertions, 57 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 62ca70626..d04887a48 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -324,7 +324,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	context
     in
     let new_type_of_hyp =
-      Reductionops.nf_betaiota sigma new_type_of_hyp in
+      Reductionops.nf_betaiota env sigma new_type_of_hyp in
     let new_ctxt,new_end_of_type =
       decompose_prod_n_assum sigma ctxt_size new_type_of_hyp
     in
@@ -698,6 +698,7 @@ let build_proof
     : tactic =
   let rec build_proof_aux do_finalize dyn_infos : tactic =
     fun g ->
+        let env = pf_env g in
         let sigma = project g in
 (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
 	match EConstr.kind sigma dyn_infos.info with
@@ -794,7 +795,7 @@ let build_proof
 		      do_finalize dyn_infos  g
 		  | Lambda _ ->
 		      let new_term =
-                        Reductionops.nf_beta sigma dyn_infos.info in
+                        Reductionops.nf_beta env sigma dyn_infos.info in
 		      build_proof do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
@@ -1153,7 +1154,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    let bodies_with_all_params =
 	      Array.map
 		(fun body ->
-		   Reductionops.nf_betaiota (project g)
+                   Reductionops.nf_betaiota (pf_env g) (project g)
 		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
 			      List.rev_map var_of_decl princ_params))
 		)
@@ -1191,12 +1192,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   let body_with_param,num =
 		     let body = get_body fnames.(i) in
 		     let body_with_full_params =
-		       Reductionops.nf_betaiota (project g) (
+                       Reductionops.nf_betaiota (pf_env g) (project g) (
 			 applist(body,List.rev_map var_of_decl full_params))
 		     in
 		     match EConstr.kind (project g) body_with_full_params with
 		       | Fix((_,num),(_,_,bs)) ->
-			       Reductionops.nf_betaiota (project g)
+                               Reductionops.nf_betaiota (pf_env g) (project g)
 				 (
 				   (applist
 				      (substl
@@ -1279,7 +1280,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       Reductionops.nf_betaiota (project g)
+                       Reductionops.nf_betaiota (pf_env g) (project g)
 			 (applist(fix_body,List.rev_map mkVar args_id));
 		     eq_hyps = []
 		   }
@@ -1339,7 +1340,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     nb_rec_hyps = -100;
 		     rec_hyps = [];
 		     info =
-		       Reductionops.nf_betaiota Evd.empty
+                       Reductionops.nf_betaiota (pf_env g) Evd.empty
 			 (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3cbb11001..acd7a30c4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -210,9 +210,9 @@ end) = struct
       let t = Reductionops.whd_all env (goalevars evars) ty in
 	match EConstr.kind (goalevars evars) t, l with
 	| Prod (na, ty, b), obj :: cstrs ->
-          let b = Reductionops.nf_betaiota (goalevars evars) b in
+          let b = Reductionops.nf_betaiota env (goalevars evars) b in
 	  if noccurn (goalevars evars) 1 b (* non-dependent product *) then
-	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
+            let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
 	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let evars, relty = mk_relty evars env ty obj in
 	    let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
@@ -221,7 +221,7 @@ end) = struct
 	    let (evars, b, arg, cstrs) =
 	      aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs
 	    in
-	    let ty = Reductionops.nf_betaiota (goalevars evars) ty in
+            let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
 	    let pred = mkLambda (na, ty, b) in
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
@@ -231,7 +231,7 @@ end) = struct
 	| _, [] ->
 	  (match finalcstr with
 	  | None | Some (_, None) ->
-	    let t = Reductionops.nf_betaiota (fst evars) ty in
+            let t = Reductionops.nf_betaiota env (fst evars) ty in
 	    let evars, rel = mk_relty evars env t None in
 	      evars, t, rel, [t, Some rel]
 	  | Some (t, Some rel) -> evars, t, rel, [t, Some rel])
@@ -1557,9 +1557,8 @@ let newfail n s =
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
   (** For compatibility *)
-  let beta_red _ sigma c = Reductionops.nf_betaiota sigma c in
-  let beta = Tactics.reduct_in_concl (beta_red, DEFAULTcast) in
-  let beta_hyp id = Tactics.reduct_in_hyp beta_red (id, InHyp) in
+  let beta = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
+  let beta_hyp id = Tactics.reduct_in_hyp Reductionops.nf_betaiota (id, InHyp) in
   let treat sigma res = 
     match res with
     | None -> newfail 0 (str "Nothing to rewrite")
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 869284246..4271c80cd 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -652,7 +652,7 @@ let decompile af =
 
 (** Backward compat to emulate the old Refine: normalize the goal conclusion *)
 let new_hole env sigma c =
-  let c = Reductionops.nf_betaiota sigma c in
+  let c = Reductionops.nf_betaiota env sigma c in
   Evarutil.new_evar env sigma c
 
 let clever_rewrite_base_poly typ p result theorem =
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 8493dbdbb..7cdf05117 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -563,7 +563,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) =
   | _ -> Constr.fold put evlist c in
   let evlist = put [] c0 in
   if evlist = [] then 0, c0 else
-  let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (project gl) (EConstr.of_constr t)) in
+  let pr_constr t = Printer.pr_econstr_env (pf_env gl) sigma (Reductionops.nf_beta (pf_env gl) (project gl) (EConstr.of_constr t)) in
   pp(lazy(str"evlist=" ++ pr_list (fun () -> str";")
     (fun (k,_) -> Evar.print k) evlist));
   let evplist = 
@@ -894,7 +894,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
       let sigma = create_evar_defs sigma in
       let (sigma, x) =
         Evarutil.new_evar env sigma
-          (if bi_types then Reductionops.nf_betaiota sigma src else src) in
+          (if bi_types then Reductionops.nf_betaiota env sigma src else src) in
       loop (EConstr.Vars.subst1 x tgt) ((m - n,x) :: args) sigma (n-1)
   | CastType (t, _) -> loop t args sigma n 
   | LetInType (_, v, _, t) -> loop (EConstr.Vars.subst1 v t) args sigma n
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1207c967b..311c1c09e 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 b646a37f8..fd83795f5 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 78de0437d..1893018a9 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 a277864c9..0565baf45 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 f682143f8..9b9408698 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 8df8f8474..e1720ec95 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 =
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 16798a1d5..9e06d913b 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -498,7 +498,7 @@ let clenv_unify_binding_type clenv c t u =
 
 let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
-  let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in
+  let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
   let c = EConstr.Unsafe.to_constr c in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 1d86a0909..5ff5fa38a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -334,7 +334,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     else
       match kind trm with
       | Meta _ ->
-	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
+        let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in
 	  if !check && occur_meta sigma conclty then
             raise (RefinerError (env, sigma, MetaInType conclty));
 	  let (gl,ev,sigma) = mk_goal hyps conclty in
@@ -416,7 +416,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
+        let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in
 	let ev = EConstr.Unsafe.to_constr ev in
 	gl::goalacc,ty,sigma,ev
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d41541251..bdcb4868b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -87,7 +87,7 @@ let pf_e_reduce = pf_apply
 let pf_whd_all         = pf_reduce whd_all
 let pf_hnf_constr                = pf_reduce hnf_constr
 let pf_nf                        = pf_reduce simpl
-let pf_nf_betaiota               = pf_reduce (fun _ -> nf_betaiota)
+let pf_nf_betaiota               = pf_reduce nf_betaiota
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 let pf_unsafe_type_of            = pf_reduce unsafe_type_of
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 22073d39b..450d68436 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1583,7 +1583,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
   let body = mkApp (lambda_create env sigma (typ,pred_body),[|dep_pair1|]) in
   let expected_goal = beta_applist sigma (abst_B,List.map fst e2_list) in
   (* Simulate now the normalisation treatment made by Logic.mk_refgoals *)
-  let expected_goal = nf_betaiota sigma expected_goal in
+  let expected_goal = nf_betaiota env sigma expected_goal in
   (* Retype to get universes right *)
   let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in
   let sigma, _ = Typing.type_of env sigma body in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4ee0a8a7b..9fded04db 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -471,7 +471,7 @@ let internal_cut_gen ?(check=true) dir replace id t =
         (if check && mem_named_context_val id sign then
 	   user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
          push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in
-    let nf_t = nf_betaiota sigma t in
+    let nf_t = nf_betaiota env sigma t in
     Proofview.tclTHEN
       (Proofview.Unsafe.tclEVARS sigma)
       (Refine.refine ~typecheck:false begin fun sigma ->
@@ -1728,7 +1728,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind :
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
 
-    let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in
+    let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in
     let try_apply thm_ty nprod =
       try
         let n = nb_prod_modulo_zeta sigma thm_ty - nprod in
@@ -1864,7 +1864,7 @@ let explain_unable_to_apply_lemma ?loc env sigma thm innerclause =
      str "."))
 
 let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
-  let thm = nf_betaiota sigma (Retyping.get_type_of env sigma d) in
+  let thm = nf_betaiota env sigma (Retyping.get_type_of env sigma d) in
   let rec aux clause =
     try progress_with_clause flags innerclause clause
     with e when CErrors.noncritical e ->
@@ -2162,7 +2162,7 @@ let apply_type newcl args =
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
     Refine.refine ~typecheck:false begin fun sigma ->
-      let newcl = nf_betaiota sigma newcl (* As in former Logic.refine *) in
+      let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in
       let (sigma, ev) =
         Evarutil.new_evar env sigma ~principal:true ~store newcl in
       (sigma, applist (ev, args))
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index e8c5aeedd..f00c1e604 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -83,12 +83,12 @@ let rec contract3' env sigma a b c = function
 
 (** Ad-hoc reductions *)
 
-let j_nf_betaiotaevar sigma j =
+let j_nf_betaiotaevar env sigma j =
   { uj_val = j.uj_val;
-    uj_type = Reductionops.nf_betaiota sigma j.uj_type }
+    uj_type = Reductionops.nf_betaiota env sigma j.uj_type }
 
-let jv_nf_betaiotaevar sigma jl =
-  Array.map (fun j -> j_nf_betaiotaevar sigma j) jl
+let jv_nf_betaiotaevar env sigma jl =
+  Array.map (fun j -> j_nf_betaiotaevar env sigma j) jl
 
 (** Printers *)
 
@@ -258,7 +258,7 @@ let explain_number_branches env sigma cj expn =
   str "expects " ++  int expn ++ str " branches."
 
 let explain_ill_formed_branch env sigma c ci actty expty =
-  let simp t = Reductionops.nf_betaiota sigma t in
+  let simp t = Reductionops.nf_betaiota env sigma t in
   let env = make_all_name_different env sigma in
   let pc = pr_leconstr_env env sigma c in
   let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
@@ -295,8 +295,8 @@ let explain_unification_error env sigma p1 p2 = function
      | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
         (* Error speaks from itself *) []
      | ConversionFailed (env,t1,t2) ->
-        let t1 = Reductionops.nf_betaiota sigma t1 in
-        let t2 = Reductionops.nf_betaiota sigma t2 in
+        let t1 = Reductionops.nf_betaiota env sigma t1 in
+        let t2 = Reductionops.nf_betaiota env sigma t2 in
         if EConstr.eq_constr sigma t1 p1 && EConstr.eq_constr sigma t2 p2 then [] else
         let env = make_all_name_different env sigma in
         if not (EConstr.eq_constr sigma t1 p1) || not (EConstr.eq_constr sigma t2 p2) then
@@ -336,8 +336,8 @@ let explain_unification_error env sigma p1 p2 = function
 
 let explain_actual_type env sigma j t reason =
   let env = make_all_name_different env sigma in
-  let j = j_nf_betaiotaevar sigma j in
-  let t = Reductionops.nf_betaiota sigma t in
+  let j = j_nf_betaiotaevar env sigma j in
+  let t = Reductionops.nf_betaiota env sigma t in
   (** Actually print *)
   let pe = pr_ne_context_of (str "In environment") env sigma in
   let pc = pr_leconstr_env env sigma (Environ.j_val j) in
@@ -351,8 +351,8 @@ let explain_actual_type env sigma j t reason =
   ppreason ++ str ".")
 
 let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
-  let randl = jv_nf_betaiotaevar sigma randl in
-  let actualtyp = Reductionops.nf_betaiota sigma actualtyp in
+  let randl = jv_nf_betaiotaevar env sigma randl in
+  let actualtyp = Reductionops.nf_betaiota env sigma actualtyp in
   let env = make_all_name_different env sigma in
   let actualtyp, exptyp = pr_explicit env sigma actualtyp exptyp in
   let nargs = Array.length randl in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1a02a22a5..fb125317e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1587,7 +1587,7 @@ let vernac_check_may_eval ~atts redexp glopt rc =
     | None ->
         let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in
         let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in
-        let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in
+        let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in
 	Feedback.msg_notice (print_judgment env sigma' j ++
                     pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++
                     Printer.pr_universe_ctx_set sigma uctx)