diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-15 22:21:22 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-15 22:21:22 +0000 |
| commit | e1a1ccd3ee9cfd72b6e9105051e5da1bf398451f (patch) | |
| tree | ad475ec7af84ae24a7f78a845f98369a63f5540f /library | |
| parent | c408060c9363eac5ff51f9a1fe8b510b1628c9f9 (diff) | |
Report improvements in Equations to the dependent elimination tactic:
- Do not touch at the user equalities and so on by using a blocking
constant. This avoids the wild autoinjections and subst tactics that
were used before. Thanks to Brian Aydemir for an example were this hurt
a lot.
- Debug the tactic used to simplify induction hypotheses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions