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 | |
| 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
| -rw-r--r-- | pretyping/evarutil.ml | 6 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 |
2 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1d5df55f3e..23f5a74c80 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -336,8 +336,10 @@ let evar_define env (ev,argsv) rhs isevars = (* the bindings to invert *) let worklist = make_subst (evar_env evi) args in let (isevars',body) = real_clean env isevars ev worklist rhs in - let isevars'' = Evd.evar_define ev body isevars' in - isevars'',[ev] + if occur_meta body then error "Meta cannot occur in evar body" + else + let isevars'' = Evd.evar_define ev body isevars' in + isevars'',[ev] (* [w_Define evd sp c] (tactic style) * 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")) |