diff options
| author | Pierre-Marie Pédrot | 2017-08-04 17:21:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-04 17:57:17 +0200 |
| commit | de88ba86e9d2a77883365503759eaec96928e9c4 (patch) | |
| tree | 02e7f58ee711af8dfdecb653821b11e083416159 /src/tac2qexpr.mli | |
| parent | 8bf0f3383fcde637ed9363f080d875a9ef0a138f (diff) | |
Introducing quotations for the rewrite tactic.
Diffstat (limited to 'src/tac2qexpr.mli')
| -rw-r--r-- | src/tac2qexpr.mli | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli index 0eb9e9f4b5..f6b8c2c19b 100644 --- a/src/tac2qexpr.mli +++ b/src/tac2qexpr.mli @@ -63,8 +63,10 @@ type hyp_location = (occurrences * Id.t located or_anti) * Locus.hyp_location_fl type clause = { q_onhyps : hyp_location list option; q_concl_occs : occurrences; } +type constr_with_bindings = (Constrexpr.constr_expr * bindings) located + type destruction_arg = -| QElimOnConstr of (Constrexpr.constr_expr * bindings) located +| QElimOnConstr of constr_with_bindings | QElimOnIdent of Id.t located | QElimOnAnonHyp of int located @@ -76,3 +78,19 @@ type induction_clause_r = { } type induction_clause = induction_clause_r located + +type multi_r = +| QPrecisely of int located +| QUpTo of int located +| QRepeatStar +| QRepeatPlus + +type multi = multi_r located + +type rewriting_r = { + rew_orient : bool option located; + rew_repeat : multi; + rew_equatn : constr_with_bindings; +} + +type rewriting = rewriting_r located |