Adding the induction and destruct tactics.

2 files changed, 48 insertions, 0 deletions

diff --git a/theories/Notations.v b/theories/Notations.v
index e7792c1555..20f01c3b48 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -96,3 +96,45 @@ Ltac2 Notation "apply"
   cb(list1(thunk(seq(constr, bindings)), ","))
   cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
   apply0 true false cb cl.
+
+Ltac2 induction0 ev ic use :=
+  let f ev use :=
+    let use := match use with
+    | None => None
+    | Some u =>
+      let ((_, c, wth)) := u in Some (c, wth)
+    end in
+    Std.induction ev ic use
+  in
+  enter_h ev f use.
+
+Ltac2 Notation "induction"
+  ic(list1(induction_clause, ","))
+  use(thunk(opt(seq("using", constr, bindings)))) :=
+  induction0 false ic use.
+
+Ltac2 Notation "einduction"
+  ic(list1(induction_clause, ","))
+  use(thunk(opt(seq("using", constr, bindings)))) :=
+  induction0 true ic use.
+
+Ltac2 destruct0 ev ic use :=
+  let f ev use :=
+    let use := match use with
+    | None => None
+    | Some u =>
+      let ((_, c, wth)) := u in Some (c, wth)
+    end in
+    Std.destruct ev ic use
+  in
+  enter_h ev f use.
+
+Ltac2 Notation "destruct"
+  ic(list1(induction_clause, ","))
+  use(thunk(opt(seq("using", constr, bindings)))) :=
+  destruct0 false ic use.
+
+Ltac2 Notation "edestruct"
+  ic(list1(induction_clause, ","))
+  use(thunk(opt(seq("using", constr, bindings)))) :=
+  destruct0 true ic use.
diff --git a/theories/Std.v b/theories/Std.v
index c2027e41c7..19bdc4c82a 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -107,6 +107,12 @@ Ltac2 @ external enough : constr -> (unit -> unit) option option -> intro_patter
 Ltac2 @ external pose : ident option -> constr -> unit := "ltac2" "tac_pose".
 Ltac2 @ external set : evar_flag -> ident option -> (unit -> constr) -> clause -> unit := "ltac2" "tac_set".
 
+Ltac2 @ external destruct : evar_flag -> induction_clause list ->
+  constr_with_bindings option -> unit := "ltac2" "tac_induction".
+
+Ltac2 @ external induction : evar_flag -> induction_clause list ->
+  constr_with_bindings option -> unit := "ltac2" "tac_induction".
+
 Ltac2 @ external red : clause -> unit := "ltac2" "tac_red".
 Ltac2 @ external hnf : clause -> unit := "ltac2" "tac_hnf".
 Ltac2 @ external cbv : red_flags -> clause -> unit := "ltac2" "tac_cbv".