diff options
| author | herbelin | 2013-02-05 16:47:04 +0000 |
|---|---|---|
| committer | herbelin | 2013-02-05 16:47:04 +0000 |
| commit | 8a590a18d267424809c9bbea5017e0d9e993c663 (patch) | |
| tree | 25932bf35329b4da7da087d95bf28518a1ae5b58 /pretyping/pretype_errors.ml | |
| parent | fb982f3d9fd7610c02ca69cad4d9c59ac26a931b (diff) | |
Revert "Ordered evars by level of dependency in the merging phase of unification"
Though this commit provides with more "natural" instances of metas
found by unification, it breaks a few contribs. The best approach to
try is maybe now to instead plug apply on evarconv.ml, rather than on
unification.ml!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16191 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions