aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Allocation.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Allocation.v')
-rw-r--r--backend/Allocation.v2
1 files changed, 2 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.