Introducing notations for destruct and induction arguments.

1 files changed, 23 insertions, 0 deletions

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;
+}