aboutsummaryrefslogtreecommitdiffstats
path: root/src/common/Monad.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/common/Monad.v')
-rw-r--r--src/common/Monad.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/common/Monad.v b/src/common/Monad.v
index c9cdc1a..1801a63 100644
--- a/src/common/Monad.v
+++ b/src/common/Monad.v
@@ -42,10 +42,10 @@ Module MonadExtra(M : Monad).
Notation "'do' X <- A ; B" :=
(bind A (fun X => B))
- (at level 200, X ident, A at level 100, B at level 200).
+ (at level 200, X name, A at level 100, B at level 200).
Notation "'do' ( X , Y ) <- A ; B" :=
(bind2 A (fun X Y => B))
- (at level 200, X ident, Y ident, A at level 100, B at level 200).
+ (at level 200, X name, Y name, A at level 100, B at level 200).
End MonadNotation.
Import MonadNotation.