diff options
| author | Jim Fehrle | 2021-01-19 11:19:33 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-01-20 12:10:08 -0800 |
| commit | cd17f9bfad72fb8f8da486facd75ff8ceecebd24 (patch) | |
| tree | 0c7f0f876b529f7b13ce707edc252d10627307db /tactics/elim.mli | |
| parent | 071c50e9c2755e93766e5fb047b0a9065934e8fe (diff) | |
Remove double induction tactic
Diffstat (limited to 'tactics/elim.mli')
| -rw-r--r-- | tactics/elim.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/elim.mli b/tactics/elim.mli index 01053502e4..a603b472f7 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -21,4 +21,3 @@ val case_tac : bool -> or_and_intro_pattern option -> val h_decompose : inductive list -> constr -> unit Proofview.tactic val h_decompose_or : constr -> unit Proofview.tactic val h_decompose_and : constr -> unit Proofview.tactic -val h_double_induction : quantified_hypothesis -> quantified_hypothesis-> unit Proofview.tactic |