diff options
Diffstat (limited to 'backend/CminorSel.v')
-rw-r--r-- | backend/CminorSel.v | 1 |
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 |