diff options
author | Yann Herklotz <git@yannherklotz.com> | 2021-10-18 17:05:46 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-18 17:05:46 +0100 |
commit | fbfa988072ce2eba808b9a6631af5f8e86cd9df0 (patch) | |
tree | 5146e558d5c9c6e9a399225eed0784b8dc12558f /src/common | |
parent | 603768a49eac2005729dd03e723ff6c5a6b292f7 (diff) | |
parent | fe06668f0de56635efe55310d7a64289a37c1d90 (diff) | |
download | vericert-fbfa988072ce2eba808b9a6631af5f8e86cd9df0.tar.gz vericert-fbfa988072ce2eba808b9a6631af5f8e86cd9df0.zip |
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'src/common')
-rw-r--r-- | src/common/Monad.v | 4 | ||||
-rw-r--r-- | src/common/Vericertlib.v | 8 |
2 files changed, 6 insertions, 6 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. diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 805dbda..331e015 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -34,7 +34,7 @@ Require Import vericert.common.Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) -Local Open Scope Z_scope. +#[local] Open Scope Z_scope. (* This tactic due to Clement Pit-Claudel with some minor additions by JDP to allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *) @@ -235,8 +235,8 @@ Ltac crush_trans := Ltac maybe t := t + idtac. -Global Opaque Nat.div. -Global Opaque Z.mul. +#[global] Opaque Nat.div. +#[global] Opaque Z.mul. Inductive Ascending : list positive -> Prop := | Ascending_nil : Ascending nil @@ -320,7 +320,7 @@ Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A) : list B := Module Notation. 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). End Notation. End Option. |