diff options
Diffstat (limited to 'src/tac2qexpr.mli')
| -rw-r--r-- | src/tac2qexpr.mli | 23 |
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; +} |