Restored a "feature" of unification in pre-8.3 (it was used e.g. in a

proof of Chung-Kil's Hur Heq package): conversion in "trivial_unify"
accepted evars as ordinary variables. I hope I did not invalidate some
features that would have needed restricting conversion on evar-free
terms, but since failure of conversion in presence of evars is redirected
to the main unification algorithm, I guess it is OK.
For better readibility, I also inlined and cleaned a bit trivial_unify.

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

0 files changed, 0 insertions, 0 deletions