diff options
| author | mohring | 2001-02-28 15:54:42 +0000 |
|---|---|---|
| committer | mohring | 2001-02-28 15:54:42 +0000 |
| commit | 05b756a9a5079e91c5015239bb801918d4903c08 (patch) | |
| tree | 465c4252b4e9d0b976369fc7b22caa132d508824 /proofs/clenv.ml | |
| 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/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 2093311851..52ce2d2ea0 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] |