diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-30 11:08:39 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-30 11:08:39 +0000 |
| commit | 3ed23b97c8d1bfbf917b540a35ee767afea28658 (patch) | |
| tree | b382d95d775b03b08a4f81b14f7517801851e139 /library/decl_kinds.ml | |
| parent | 10fa0c0b6b6d29901de9258d7fad402e3b6ec79a (diff) | |
Improve the dependent induction tactic to automatically find the
generalized hypotheses. Also move part of the tactic to ML and
improve the generated proof term in case of non-dependent induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11023 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/decl_kinds.ml')
0 files changed, 0 insertions, 0 deletions