aboutsummaryrefslogtreecommitdiff
path: root/src/tac2qexpr.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-09-03 19:45:23 +0200
committerPierre-Marie Pédrot2017-09-03 23:43:50 +0200
commit65daf8fca747d385b2985e4e5e91894738f6fcf1 (patch)
tree622f42103d2c79b1742b093ec972016bd4704221 /src/tac2qexpr.mli
parenta2302a48a96a6b635f5301f7cc6254acb58211bc (diff)
Introducing a macro for constr matching.
Diffstat (limited to 'src/tac2qexpr.mli')
-rw-r--r--src/tac2qexpr.mli8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 7c774a5c80..a284c1e756 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -115,3 +115,11 @@ type red_flag_r =
type red_flag = red_flag_r located
type strategy_flag = red_flag list located
+
+type constr_match_branch_r =
+| QConstrMatchPattern of Constrexpr.constr_expr * raw_tacexpr
+| QConstrMatchContext of Id.t option * Constrexpr.constr_expr * raw_tacexpr
+
+type constr_match_branch = constr_match_branch_r located
+
+type constr_matching = constr_match_branch list located