From 1bceed4982aa9f0e32478f3b75f287836e00e713 Mon Sep 17 00:00:00 2001
From: Hai Dang <haidang@mpi-sws.org>
Date: Sun, 26 Jan 2025 18:56:51 +0100
Subject: [PATCH] fix several warnings

---
 gpfsl-examples/sflib.v       | 2 +-
 gpfsl/algebra/lattice_cmra.v | 2 +-
 gpfsl/gps/cbends.v           | 2 +-
 gpfsl/orc11/base.v           | 2 +-
 gpfsl/orc11/progress.v       | 4 ++--
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/gpfsl-examples/sflib.v b/gpfsl-examples/sflib.v
index 4c9559a4..8e3dbea3 100644
--- a/gpfsl-examples/sflib.v
+++ b/gpfsl-examples/sflib.v
@@ -11,7 +11,7 @@
 
 (** Symbols starting with [sflib__] are internal. *)
 
-Require Import Bool List Arith ZArith String Program.
+From Stdlib Require Import Bool List Arith ZArith String Program.
 (* Require Export paconotation newtac. *)
 
 Set Implicit Arguments.
diff --git a/gpfsl/algebra/lattice_cmra.v b/gpfsl/algebra/lattice_cmra.v
index e8d00bd8..46ca571b 100644
--- a/gpfsl/algebra/lattice_cmra.v
+++ b/gpfsl/algebra/lattice_cmra.v
@@ -148,7 +148,7 @@ Section lat_auth.
   Qed.
 End lat_auth.
 
-From Coq.QArith Require Import Qcanon.
+From Stdlib.QArith Require Import Qcanon.
 
 Lemma frac_prod_max {A : cmra} (q: frac) (a b : A) :
   ✓ (q, a) → (1%Qp, b) ≼ (q, a) → False.
diff --git a/gpfsl/gps/cbends.v b/gpfsl/gps/cbends.v
index 6101aa33..a133c286 100644
--- a/gpfsl/gps/cbends.v
+++ b/gpfsl/gps/cbends.v
@@ -1,4 +1,4 @@
-From Coq.QArith Require Import Qcanon.
+From Stdlib.QArith Require Import Qcanon.
 From gpfsl.lang Require Import lang.
 From gpfsl.gps Require Export block_ends.
 
diff --git a/gpfsl/orc11/base.v b/gpfsl/orc11/base.v
index dd3f4e93..7a74fec3 100644
--- a/gpfsl/orc11/base.v
+++ b/gpfsl/orc11/base.v
@@ -1,4 +1,4 @@
-From Coq Require Export Utf8 ssreflect.
+From Stdlib Require Export Utf8 ssreflect.
 From stdpp Require Export prelude finite gmap.
 From stdpp Require Import sorting.
 
diff --git a/gpfsl/orc11/progress.v b/gpfsl/orc11/progress.v
index 3fc8d359..2935f034 100644
--- a/gpfsl/orc11/progress.v
+++ b/gpfsl/orc11/progress.v
@@ -638,7 +638,7 @@ Section AllocSteps.
   Proof.
     move => 𝑚s.
     constructor; last done.
-    - by rewrite map_length length_seq.
+    - by rewrite length_map length_seq.
     - move => n' 𝑚 Eq.
       rewrite /𝑚s /alloc_messages in Eq.
       apply list_lookup_fmap_inv in Eq as [i [Eq1 [Eq2 Lt]%lookup_seq]].
@@ -801,7 +801,7 @@ Section AllocSteps.
     move => 𝑚s.
     have REMOVE:= dealloc_remove _ _ _ DEALLOC.
     constructor; last done.
-    - by rewrite map_length length_seq.
+    - by rewrite length_map length_seq.
     - move => n' 𝑚 Eq. rewrite /𝑚s /dealloc_messages in Eq.
       apply list_lookup_fmap_inv in Eq as [i [Eq1 [Eq2 Lt]%lookup_seq]].
       simpl in Eq2. subst i.
-- 
GitLab