diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-06 21:25:52 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-06 21:25:52 +0000 |
| commit | 6160f53e89800a785d773c4130b08fbe7c345651 (patch) | |
| tree | 88b2aadfa1c697ca8686818be25fcf9449b5dba6 /proofs/logic.ml | |
| 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/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 7755efeb5..7424685bc 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 |