From fce4a1a9cbb57a636155181898ae4ecece5af59d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 4 Aug 2017 13:04:10 +0200
Subject: Adding the induction and destruct tactics.

---
 src/tac2tactics.mli | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'src/tac2tactics.mli')

diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 86278f177e..f29793411a 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -16,3 +16,12 @@ open Proofview
 val apply : advanced_flag -> evars_flag ->
   EConstr.constr with_bindings tactic list ->
   (Id.t * intro_pattern option) option -> unit tactic
+
+type induction_clause =
+  EConstr.constr with_bindings tactic destruction_arg *
+  intro_pattern_naming option *
+  or_and_intro_pattern option *
+  Locus.clause option
+
+val induction_destruct : rec_flag -> evars_flag ->
+  induction_clause list -> EConstr.constr with_bindings option -> unit Proofview.tactic
-- 
cgit v1.2.3