Fix warnings for Coq 8.13.2

2 files changed, 6 insertions, 6 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.
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index b58ebd4..389a74f 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 *)
@@ -190,8 +190,8 @@ Ltac liapp :=
 Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
               try assumption; try (solve [auto]).
 
-Global Opaque Nat.div.
-Global Opaque Z.mul.
+#[global] Opaque Nat.div.
+#[global] Opaque Z.mul.
 
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
@@ -231,7 +231,7 @@ Definition join {A : Type} (a : option (option A)) : option A :=
 
 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.