Merge branch 'master' into dev/michalisdev/michalis

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.