diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-03 15:21:05 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-10-03 15:21:05 +0000 |
| commit | 66ee4884f2c301eeac1f73deb97d6b50d1faa8bd (patch) | |
| tree | 2a560e56d366ef92c86985595e5e1f708b6b3243 /kernel | |
| parent | 6832c60f741e6bfb2a850d567fd6a1dff7059393 (diff) | |
(Try to) use the conversion oracle also in w_unify to choose which constant to
unfold first. The patch changes the usual order of unifications so some
may differ (only one example in the stdlib breaks because of more
unification happening).
Actually this change was trigerred because of an incompleteness which is
not resolved here. At least this way unfolding is consistent between
w_unify and the kernel.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions