From b84b03bb6230fca69cd9191ba0424402a5cd2330 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 3 Aug 2017 20:23:08 +0200
Subject: Introducing notations for destruct and induction arguments.

---
 theories/Std.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'theories')

diff --git a/theories/Std.v b/theories/Std.v
index 3d1e8f462d..c2027e41c7 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -73,6 +73,19 @@ with or_and_intro_pattern := [
 | IntroAndPattern (intro_pattern list)
 ].
 
+Ltac2 Type destruction_arg := [
+| ElimOnConstr (unit -> constr_with_bindings)
+| ElimOnIdent (ident)
+| ElimOnAnonHyp (int)
+].
+
+Ltac2 Type induction_clause := {
+  indcl_arg : destruction_arg;
+  indcl_eqn : intro_pattern_naming option;
+  indcl_as : or_and_intro_pattern option;
+  indcl_in : clause option;
+}.
+
 Ltac2 Type evar_flag := bool.
 Ltac2 Type advanced_flag := bool.
 
-- 
cgit v1.2.3