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/evarutil.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/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 6 |
1 files changed, 4 insertions, 2 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) * |