diff options
| author | barras | 2009-02-06 21:25:52 +0000 |
|---|---|---|
| committer | barras | 2009-02-06 21:25:52 +0000 |
| commit | 6160f53e89800a785d773c4130b08fbe7c345651 (patch) | |
| tree | 88b2aadfa1c697ca8686818be25fcf9449b5dba6 /proofs | |
| parent | 370575d3e98f375969983d26f62a1ddeab524d0e (diff) | |
pushed evar reduction in kernel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11889 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 6 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 7755efeb52..7424685bc9 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -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 7240e8b858..7a66067cd7 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -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 45bd0c8962..19ea5c398d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -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 |