diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocation.v | 2 | ||||
| -rw-r--r-- | backend/CminorSel.v | 1 | ||||
| -rw-r--r-- | backend/Registers.v | 2 |
3 files changed, 5 insertions, 0 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 08e0a4f4..4de215b8 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -167,6 +167,8 @@ Definition check_succ (s: node) (b: LTL.bblock) : bool := | _ => false end. +Declare Scope option_monad_scope. + Notation "'do' X <- A ; B" := (match A with Some X => B | None => None end) (at level 200, X ident, A at level 100, B at level 200) : option_monad_scope. 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 diff --git a/backend/Registers.v b/backend/Registers.v index 622cddfe..7f7ecb60 100644 --- a/backend/Registers.v +++ b/backend/Registers.v @@ -61,6 +61,8 @@ Definition regmap_setres | _ => rs end. +Declare Scope rtl. + Notation "a # b" := (Regmap.get b a) (at level 1) : rtl. Notation "a ## b" := (List.map (fun r => Regmap.get r a) b) (at level 1) : rtl. Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level) : rtl. |