diff options
| author | sacerdot | 2005-05-24 16:11:37 +0000 |
|---|---|---|
| committer | sacerdot | 2005-05-24 16:11:37 +0000 |
| commit | 6f05eae01aedd4e477030be8a461d17939fc3b72 (patch) | |
| tree | 1e342dc443f1571f0dbb6925d53db493f885316f /pretyping/unification.ml | |
| parent | d2331067061699e2cd105bf88d8361ed45fa6f3d (diff) | |
WARNING: unification changed (to fix a bug).
1. When matching ?i[sigma] against t' in some cases ?i was instantiated with t'
ignoring the explicit substitution sigma (i.e. always doing mimick); however,
when t' occurs in sigma ?i can be instatiated with a Var/Rel (i.e. doing
projection).
The new behaviour is not equivalent to the old one (even up to bugs) since
the new behaviour may accept not well typed instantiations and fail only
later whereas the old (but buggy) behaviour failed immediately.
2. Second bug fixed: it was the case that instantiating and evar doing
projection did not check whether the body of the evar contained
metavariables (that breaks a Coq invariant).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7067 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b5e175dd82..2801d3ee49 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -224,14 +224,14 @@ let w_merge env with_types mod_delta metas evars evd = match krhs with | App (f,cl) when is_mimick_head f -> (try - w_merge_rec (w_Define evn rhs' evd) metas t + w_merge_rec (fst (evar_define env ev rhs' evd)) metas t with ex when precatchable_exception ex -> let evd' = mimick_evar evd mod_delta f (Array.length cl) evn in w_merge_rec evd' metas evars) | _ -> (* ensure tail recursion in non-mimickable case! *) - w_merge_rec (w_Define evn rhs' evd) metas t + w_merge_rec (fst (evar_define env ev rhs' evd)) metas t end | _ -> anomaly "w_merge_rec")) |