diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-09 14:30:03 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-09 14:30:03 +0100 |
| commit | f06e5fc0ee651c3ffe357c3c3302ca1517381b4c (patch) | |
| tree | 15821bec5295bc84b95bd44b00e0d192c58c36fe /src/common/Monad.v | |
| parent | ce3adde4b50ba04430a1cf0ffb0ea85168091746 (diff) | |
| download | vericert-f06e5fc0ee651c3ffe357c3c3302ca1517381b4c.tar.gz vericert-f06e5fc0ee651c3ffe357c3c3302ca1517381b4c.zip | |
Fix warnings for Coq 8.13.2
Diffstat (limited to 'src/common/Monad.v')
| -rw-r--r-- | src/common/Monad.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/common/Monad.v b/src/common/Monad.v index 5e8385e..fcbe527 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -40,10 +40,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. |