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.

---
 src/tac2qexpr.mli | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'src/tac2qexpr.mli')

diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index b68efe73ac..5075f2d7d4 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -40,3 +40,26 @@ and intro_pattern_action =
 and or_and_intro_pattern =
 | QIntroOrPattern of intro_pattern list list
 | QIntroAndPattern of intro_pattern list
+
+type occurrences =
+| QAllOccurrences
+| QAllOccurrencesBut of int or_anti list
+| QNoOccurrences
+| QOnlyOccurrences of int or_anti list
+
+type hyp_location = (occurrences * Id.t or_anti) * Locus.hyp_location_flag
+
+type clause =
+  { q_onhyps : hyp_location list option; q_concl_occs : occurrences; }
+
+type destruction_arg =
+| QElimOnConstr of Constrexpr.constr_expr * bindings
+| QElimOnIdent of Id.t
+| QElimOnAnonHyp of int
+
+type induction_clause = {
+  indcl_arg : destruction_arg;
+  indcl_eqn : intro_pattern_naming option;
+  indcl_as : or_and_intro_pattern option;
+  indcl_in : clause option;
+}
-- 
cgit v1.2.3