aboutsummaryrefslogtreecommitdiffstats
path: root/backend/CminorSel.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/CminorSel.v')
-rw-r--r--backend/CminorSel.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index f6f6e34d..97a666bd 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -54,6 +54,7 @@ with condexpr : Type :=
| CEcondition : condexpr -> condexpr -> condexpr -> condexpr
| CElet: expr -> condexpr -> condexpr.
+Declare Scope cminorsel_scope.
Infix ":::" := Econs (at level 60, right associativity) : cminorsel_scope.
(** Conditional expressions [condexpr] are expressions that are evaluated