The ad hoc version for first-order unification at toplevel of "?n args

= t" introduced in r14199 (w_typed_unify_list) tried to check types of
metas more than what w_typed_unify used to before (and these types
need delta to be convertible). Don't know if it is a weakness of the
test for checking types but since checking types should not be
necessary here, w_typed_unify_list now follows what w_unify_core_0
does more closely.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14217 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions