diff --git a/gpfsl-examples/sflib.v b/gpfsl-examples/sflib.v
index 4c9559a46c62a14c56f96ff4fc8590ed88cc77e0..8e3dbea3f8aa5eab4ba16dc8371627b01a6581d1 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 e8d00bd88a550e721231dc6b3564a2905fe64ec5..46ca571b28a0ed7ddc9f7f66146e1054fdac2fcf 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 6101aa33d4829652837e61a2b5ff15f6c880b37d..a133c286f13aef2f080393f34e86d2de4465004c 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/logic/relacq.v b/gpfsl/logic/relacq.v
index d7dc2427eeb4e400a007d06fe8ede7b5108bb8af..344530b5b4eea3c27e4a0e16e9795ed7cfbdd989 100644
--- a/gpfsl/logic/relacq.v
+++ b/gpfsl/logic/relacq.v
@@ -55,7 +55,6 @@ Section RelAcqProp.
   Proof.
     unseal. iIntros "obj".
     iExists ∅. rewrite -view_at_objectively. iFrame "obj".
-    rewrite (_: (◯ to_latT (∅: threadView) : authR _) = ε) //.
     rewrite -embed_bupd. by iApply own_unit.
   Qed.
 
diff --git a/gpfsl/orc11/base.v b/gpfsl/orc11/base.v
index dd3f4e9379240004515e35d432ce98793b553e11..7a74fec30fcd8b2ff8ed8dec1fab7573cf91f01a 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 3fc8d359ee570305ef2a25ec009006d263486e89..2935f0345e502f2206e30c1cbb8d763d2874d924 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.