diff options
| author | barras | 2002-03-05 10:09:10 +0000 |
|---|---|---|
| committer | barras | 2002-03-05 10:09:10 +0000 |
| commit | 21cd39996cabdf280f4cc99557c54f6c7c73bbc8 (patch) | |
| tree | be8d5b416b16098afb414195bc14123e62d1ffe6 | |
| parent | 337bc5b7c8711683c493f314e25722df49f385c8 (diff) | |
unification faite de gauche a droite (et non pas l'inverse) pour eviter que
clenv_typed_unify plante trop facilement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2511 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/clenv.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d7082d19a0..f47156190a 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -264,7 +264,7 @@ let unify_0 cv_pb mc wc m n = let rec w_Unify cv_pb m n mc wc = let (mc',ec') = unify_0 cv_pb mc wc m n in - w_resrec mc' ec' wc + w_resrec (List.rev mc') (List.rev ec') wc and w_resrec metas evars wc = match evars with @@ -609,7 +609,7 @@ let clenv_merge with_types = | Evar (evn,_) -> if w_defined_evar clenv.hook evn then let (metas',evars') = unify_0 CONV [] clenv.hook rhs lhs in - clenv_resrec (metas'@metas) (evars'@t) clenv + clenv_resrec (List.rev metas'@metas) (List.rev evars'@t) clenv else begin let rhs' = if occur_meta rhs then subst_meta metas rhs else rhs @@ -634,7 +634,7 @@ let clenv_merge with_types = if clenv_defined clenv mv then let (metas',evars') = unify_0 CONV [] clenv.hook (clenv_value clenv mv).rebus n in - clenv_resrec (metas'@t) evars' clenv + clenv_resrec (List.rev metas'@t) (List.rev evars') clenv else let mc,ec = let mvty = clenv_instance_type clenv mv in @@ -645,7 +645,8 @@ let clenv_merge with_types = unify_0 CUMUL [] clenv.hook nty mvty with e when Logic.catchable_exception e -> ([],[])) else ([],[]) in - clenv_resrec (mc@t) ec (clenv_assign mv n clenv) + clenv_resrec (List.rev mc@t) (List.rev ec) + (clenv_assign mv n clenv) in clenv_resrec @@ -661,7 +662,7 @@ let clenv_merge with_types = let clenv_unify_core_0 with_types cv_pb m n clenv = let (mc,ec) = unify_0 cv_pb [] clenv.hook m n in - clenv_merge with_types mc ec clenv + clenv_merge with_types (List.rev mc) (List.rev ec) clenv let clenv_unify_0 = clenv_unify_core_0 false let clenv_typed_unify = clenv_unify_core_0 true |