diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-05 22:43:56 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-05 22:43:56 +0000 |
| commit | dd7a12f1a2caddef510ad857f0183ae3501b05ac (patch) | |
| tree | 5346794991eea35ae0b0e34840b5c7b4d8f13604 /library/libobject.ml | |
| parent | 02a8749f2be324b2fe85897af17d9943dfcd08d7 (diff) | |
Correctly do backtracking during type class resolution even if only new
existentials are generated (at last!). The code simply keeps failure
continuations and apply them if needed.
Fix bottomup and topdown rewrite strategies that looped.
Use auto introduction flag for typeclass instances as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12374 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/libobject.ml')
0 files changed, 0 insertions, 0 deletions