From e6353e9ef6542b444391a46d9557ebf3a6443947 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 2 Feb 2018 15:55:54 +0100
Subject: Reductionops.nf_* now take an environment.

---
 proofs/clenv.ml   | 2 +-
 proofs/logic.ml   | 4 ++--
 proofs/tacmach.ml | 2 +-
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3