aboutsummaryrefslogtreecommitdiffstats
path: root/common/Errors.v
diff options
context:
space:
mode:
Diffstat (limited to 'common/Errors.v')
-rw-r--r--common/Errors.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/common/Errors.v b/common/Errors.v
index bf72f12b..d9158165 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -67,6 +67,8 @@ Definition bind2 (A B C: Type) (f: res (A * B)) (g: A -> B -> res C) : res C :=
(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
+Declare Scope error_monad_scope.
+
Notation "'do' X <- A ; B" := (bind A (fun X => B))
(at level 200, X ident, A at level 100, B at level 200)
: error_monad_scope.