Binding the inversion family of tactics.

2 files changed, 26 insertions, 0 deletions

diff --git a/theories/Notations.v b/theories/Notations.v
index 75abb2f1cd..8a3e769d12 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -298,6 +298,24 @@ Ltac2 Notation "edestruct"
   use(thunk(opt(seq("using", constr, with_bindings)))) :=
   destruct0 true ic use.
 
+Ltac2 Notation "simple" "inversion"
+  arg(destruction_arg)
+  pat(opt(seq("as", intropattern)))
+  ids(opt(seq("in", list1(ident)))) :=
+  Std.inversion Std.SimpleInversion arg pat ids.
+
+Ltac2 Notation "inversion"
+  arg(destruction_arg)
+  pat(opt(seq("as", intropattern)))
+  ids(opt(seq("in", list1(ident)))) :=
+  Std.inversion Std.FullInversion arg pat ids.
+
+Ltac2 Notation "inversion_clear"
+  arg(destruction_arg)
+  pat(opt(seq("as", intropattern)))
+  ids(opt(seq("in", list1(ident)))) :=
+  Std.inversion Std.FullInversionClear arg pat ids.
+
 Ltac2 default_on_concl cl :=
 match cl with
 | None => { Std.on_hyps := Some []; Std.on_concl := Std.AllOccurrences }
diff --git a/theories/Std.v b/theories/Std.v
index b63c2eaa41..02bc4ff450 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -106,6 +106,12 @@ Ltac2 Type rewriting := {
 Ltac2 Type evar_flag := bool.
 Ltac2 Type advanced_flag := bool.
 
+Ltac2 Type inversion_kind := [
+| SimpleInversion
+| FullInversion
+| FullInversionClear
+].
+
 (** Standard, built-in tactics. See Ltac1 for documentation. *)
 
 Ltac2 @ external intros : evar_flag -> intro_pattern list -> unit := "ltac2" "tac_intros".
@@ -197,6 +203,8 @@ Ltac2 @ external exact_no_check : constr -> unit := "ltac2" "tac_exactnocheck".
 Ltac2 @ external vm_cast_no_check : constr -> unit := "ltac2" "tac_vmcastnocheck".
 Ltac2 @ external native_cast_no_check : constr -> unit := "ltac2" "tac_nativecastnocheck".
 
+Ltac2 @ external inversion : inversion_kind -> destruction_arg -> intro_pattern option -> ident list option -> unit := "ltac2" "tac_inversion".
+
 (** coretactics *)
 
 (** extratactics *)