diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-28 15:54:42 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-28 15:54:42 +0000 |
| commit | 05b756a9a5079e91c5015239bb801918d4903c08 (patch) | |
| tree | 465c4252b4e9d0b976369fc7b22caa132d508824 /proofs | |
| parent | d942d0d429023bddd7ea93f4435d42357b296b23 (diff) | |
introduction d'un refine avec resolution des types et de l'instantiation des metas dans les existentielles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 11 | ||||
| -rw-r--r-- | proofs/logic.ml | 3 | ||||
| -rw-r--r-- | proofs/refiner.ml | 5 |
3 files changed, 11 insertions, 8 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 209331185..52ce2d2ea 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -153,7 +153,7 @@ let unify_0 mc wc m n = raise ex in - if (not((occur_meta m))) & is_conv env sigma m n then + if (not(occur_meta m)) & is_conv env sigma m n then (mc,[]) else unirec_rec (mc,[]) m n @@ -557,9 +557,9 @@ let clenv_merge with_types = let (metas',evars') = unify_0 [] clenv.hook rhs lhs in clenv_resrec (metas'@metas) (evars'@t) clenv else - (try + (try let rhs' = if occur_meta rhs then subst_meta metas rhs else rhs in clenv_resrec metas t - (clenv_wtactic (w_Define evn rhs) clenv) + (clenv_wtactic (w_Define evn rhs') clenv) with ex when catchable_exception ex -> (match krhs with | IsApp (f,cl) when isConst f or isMutConstruct f -> @@ -580,9 +580,11 @@ let clenv_merge with_types = let mc,ec = let mvty = clenv_instance_type clenv mv in if with_types (* or occur_meta mvty *) then + (try let nty = clenv_type_of clenv (clenv_instance clenv (mk_freelisted n)) in unify_0 [] clenv.hook mvty nty + with e when Logic.catchable_exception e -> ([],[])) else ([],[]) in clenv_resrec (mc@t) ec (clenv_assign mv n clenv) @@ -602,7 +604,8 @@ let clenv_unify_core with_types m n clenv = let (mc,ec) = unify_0 [] clenv.hook m n in clenv_merge with_types mc ec clenv -let clenv_unify = clenv_unify_core false +(* let clenv_unify = clenv_unify_core false *) +let clenv_unify = clenv_unify_core true let clenv_typed_unify = clenv_unify_core true (* [clenv_bchain mv clenv' clenv] diff --git a/proofs/logic.ml b/proofs/logic.ml index 97590bfb4..0f1d2c84c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -63,7 +63,8 @@ let conv_leq_goal env sigma arg ty conclty = let rec mk_refgoals sigma goal goalacc conclty trm = let env = evar_env goal in let hyps = goal.evar_hyps in -(* if not (occur_meta trm) then +(* + if not (occur_meta trm) then let t'ty = (unsafe_machine env sigma trm).uj_type in let _ = conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 37a41cd25..e9c214753 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -664,12 +664,11 @@ let extract_pftreestate pts = if subgoals <> [] then errorlabstrm "extract_proof" [< 'sTR "Attempt to save an incomplete proof" >]; - (*** let env = Global.env_of_context pts.tpf.goal.evar_hyps in strong whd_betaiotaevar env (ts_it pts.tpfsigma) pfterm - ***) + (*** local_strong (whd_ise (ts_it pts.tpfsigma)) pfterm - + ***) (* Focus on the first leaf proof in a proof-tree state *) let rec first_unproven pts = |