summaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/logic.ml8
-rw-r--r--proofs/refiner.ml4
-rw-r--r--proofs/tacmach.ml4
3 files changed, 8 insertions, 8 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a04216cb..3e758eb6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
+(* $Id: logic.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
*)
match kind_of_term trm with
| Meta _ ->
- let conclty = nf_betaiota conclty in
+ let conclty = nf_betaiota sigma conclty in
if !check && occur_meta conclty then
raise (RefinerError (MetaInType conclty));
(mk_goal hyps conclty)::goalacc, conclty
@@ -390,7 +390,7 @@ and mk_hdgoals sigma goal goalacc trm =
match kind_of_term trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
- (mk_goal hyps (nf_betaiota ty))::goalacc,ty
+ (mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty
| Cast (t,_, ty) ->
check_typability env sigma ty;
@@ -502,7 +502,7 @@ let prim_refiner r sigma goal =
raise (RefinerError IntroNeedsProduct))
| Cut (b,replace,id,t) ->
- let sg1 = mk_goal sign (nf_betaiota t) in
+ let sg1 = mk_goal sign (nf_betaiota sigma t) in
let sign,cl,sigma =
if replace then
let nexthyp = get_hyp_after id (named_context_of_val sign) in
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a9a1f51d..7ce256bf 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml 11865 2009-01-28 17:34:30Z herbelin $ *)
+(* $Id: refiner.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -763,7 +763,7 @@ let extract_pftreestate pts =
else
str "Attempt to save a proof with existential variables still non-instantiated");
let env = Global.env_of_context pts.tpf.goal.evar_hyps in
- nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm
+ nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm
(* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
(***
local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index bf194d47..6c4f7b5e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacmach.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(* $Id: tacmach.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -99,7 +99,7 @@ let pf_whd_betadeltaiota_stack = pf_reduce whd_betadeltaiota_stack
let pf_hnf_constr = pf_reduce hnf_constr
let pf_red_product = pf_reduce red_product
let pf_nf = pf_reduce nf
-let pf_nf_betaiota = pf_reduce (fun _ _ -> nf_betaiota)
+let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota)
let pf_compute = pf_reduce compute
let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds)
let pf_type_of = pf_reduce type_of