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

0 files changed, 0 insertions, 0 deletions