diff options
author | 2008-09-25 20:25:06 +0000 | |
---|---|---|
committer | 2008-09-25 20:25:06 +0000 | |
commit | e3535ade2bd4c7b75ec093e9e0f124f84c506b8f (patch) | |
tree | e6ace79e3a52db095645cce68450593758da89e4 /tools/coqdoc/main.ml | |
parent | b103459011e65c09d481bdaee5fd7ce7638fb139 (diff) |
Various little improvements:
- A new [dependent pattern] tactic to do a pattern on an object in an
inductive family and generalize by both the indexes and the object
itself. Useful to prepare a goal for elimination with a dependent
principle.
- Better dependent elimination simplification tactic that doesn't
throw away non-dependent equalities if they can't be injected.
- Add [fold_sub] and [unfold_sub] tactics for folding/unfolding
well-founded definitions using measures built by Program.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11420 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/main.ml')
0 files changed, 0 insertions, 0 deletions