diff options
| author | Pierre-Marie Pédrot | 2017-10-30 15:53:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-30 17:12:16 +0100 |
| commit | a997ee7d78d90740b15b58502a1dc5e587b43ee3 (patch) | |
| tree | 0af87e2a77690deda29bec02a978076dd8f89d7e /src/tac2qexpr.mli | |
| parent | f18502f32fb25b29cafe26340edbbcedd463c646 (diff) | |
Introducing the change tactic.
Diffstat (limited to 'src/tac2qexpr.mli')
| -rw-r--r-- | src/tac2qexpr.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli index 229cece7c4..ad52884ca6 100644 --- a/src/tac2qexpr.mli +++ b/src/tac2qexpr.mli @@ -84,6 +84,12 @@ type induction_clause_r = { type induction_clause = induction_clause_r located +type conversion_r = +| QConvert of Constrexpr.constr_expr +| QConvertWith of Constrexpr.constr_expr * Constrexpr.constr_expr + +type conversion = conversion_r located + type multi_r = | QPrecisely of int located | QUpTo of int located |