diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 19:08:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 19:08:35 +0000 |
| commit | 8556f4e4b5e21535013e6962feabfede6313462b (patch) | |
| tree | 447db6ec6d94524906d66238638f1c22e74518f5 /pretyping/cases.mli | |
| parent | e46a343090514c1340d4e5b97384b55b42c9c166 (diff) | |
Backtracking on the use of automatically generated schemes for
"eq"-rewriting (a few contributions are still referring explicitly to
eq_rect, eq_ind and co and the new mechanism, though working also for
dependent rewriting, is not powerful enough in general wrt fixpoint
guard to claim being uniformly better).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12501 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/cases.mli')
0 files changed, 0 insertions, 0 deletions