diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-30 04:21:51 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-30 04:21:51 +0000 |
| commit | 2b9f73c7e86ac718c0ce4c47d6a24ffc2d01499d (patch) | |
| tree | 4036fe3c992e406c790d165b17424c3530653277 /tactics | |
| parent | 90b063be6b3c23a54e1d59974e09ee14f2941338 (diff) | |
Work on dependent induction tactic and friends, finish the test-suite example
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10487 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index db46c621f..eb62f602a 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -327,11 +327,4 @@ val tclABSTRACT : identifier option -> tactic -> tactic val admit_as_an_axiom : tactic -val make_abstract_generalize : 'a -> - Names.identifier -> - Term.constr -> - Sign.rel_context -> - Term.types -> - Term.types list -> - Term.constr list -> Term.constr list -> Term.constr -> Term.constr val abstract_generalize : identifier -> tactic |