diff --git a/_CoqProject b/_CoqProject
index 38bffb8d3d20e388a1d41da67a101b9d6f9443ae..0c42e93be8e3fbf59374ed8a8d42590d41ce5d3e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,6 +3,7 @@
 -arg -w -arg -notation-overridden
 # non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
 -arg -w -arg -redundant-canonical-projection
+-arg -w -arg -projection-no-head-constant
 # change_no_check does not exist yet in 8.9.
 -arg -w -arg -convert_concl_no_check
 # "Declare Scope" does not exist yet in 8.9.
diff --git a/theories/hocap/cg_bag.v b/theories/hocap/cg_bag.v
index 062227ab2eacc2cbb9308650a92deb4f2c37e4c0..180eecfbf59788608e6eefebc79e9b2579a1b01f 100644
--- a/theories/hocap/cg_bag.v
+++ b/theories/hocap/cg_bag.v
@@ -66,7 +66,7 @@ Section proof.
   Definition is_bag (γb : gname) (x : val) :=
 
     (∃ (lk : val) (b : loc) (γ : gname),
-        ⌜x = PairV #b lk⌝ ∗ is_lock N γ lk (bag_inv γb b))%I.
+        ⌜x = PairV #b lk⌝ ∗ is_lock γ lk (bag_inv γb b))%I.
   Definition bag_contents (γb : gname) (X : gmultiset val) : iProp Σ :=
     own γb ((1/2)%Qp, to_agree X).
 
@@ -106,7 +106,7 @@ Section proof.
     unfold newBag. wp_rec.
     wp_alloc r as "Hr". wp_let.
     iMod (own_alloc (1%Qp, to_agree ∅)) as (γb) "[Ha Hf]"; first done.
-    wp_apply (newlock_spec N (bag_inv γb r) with "[Hr Ha]").
+    wp_apply (newlock_spec (bag_inv γb r) with "[Hr Ha]").
     { iExists []. iFrame. }
     iIntros (lk γ) "#Hlk". wp_pures. iApply "HΦ".
     rewrite /is_bag /bag_contents. iFrame.
@@ -176,11 +176,11 @@ End proof.
 Typeclasses Opaque bag_contents is_bag.
 
 Canonical Structure cg_bag `{!heapG Σ, !bagG Σ} : bag Σ :=
-  {| abstract_bag.is_bag := is_bag;
-     abstract_bag.is_bag_persistent := is_bag_persistent;
+  {| abstract_bag.is_bag N := is_bag;
+     abstract_bag.is_bag_persistent N := is_bag_persistent;
      abstract_bag.bag_contents_timeless := bag_contents_timeless;
      abstract_bag.bag_contents_agree := bag_contents_agree;
      abstract_bag.bag_contents_update := bag_contents_update;
-     abstract_bag.newBag_spec := newBag_spec;
+     abstract_bag.newBag_spec N := newBag_spec;
      abstract_bag.pushBag_spec := pushBag_spec;
      abstract_bag.popBag_spec := popBag_spec |}.
diff --git a/theories/logatom/flat_combiner/flat.v b/theories/logatom/flat_combiner/flat.v
index 67df130f8d4f0a67f6caed27b7961a97c0f952ef..6beef55f2f17d780de261ecc76d9e61f7409d482 100644
--- a/theories/logatom/flat_combiner/flat.v
+++ b/theories/logatom/flat_combiner/flat.v
@@ -212,7 +212,7 @@ Section proof.
 
   Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
     inv N (srv_bag R γm γr s) ∗
-    is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ Φ #()
+    is_lock γlk lk (own γr (Excl ()) ∗ R) ∗ Φ #()
     ⊢ WP try_srv lk #s {{ Φ }}.
   Proof.
     iIntros "(#? & #? & HΦ)". wp_lam. wp_pures.
@@ -237,7 +237,7 @@ Section proof.
   Lemma loop_spec R (p s: loc) (lk: val)
         (γs γr γm γlk: gname) (ts: toks):
     {{{ inv N (srv_bag R γm γr s) ∗ inv N (p_inv R γm γr ts p) ∗
-        is_lock N γlk lk (own γr (Excl ()) ∗ R) ∗ own_γ3 ts }}}
+        is_lock γlk lk (own γr (Excl ()) ∗ R) ∗ own_γ3 ts }}}
       loop #p #s lk
     {{{ x y, RET y; finished_recp ts x y }}}.
   Proof.
@@ -272,7 +272,7 @@ Section proof.
     iIntros (R Φ) "HR HΦ".
     iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
     wp_lam. wp_bind (newlock _).
-    iApply (newlock_spec _ (own γr (Excl ()) ∗ R)%I with "[$Ho2 $HR]")=>//.
+    iApply (newlock_spec (own γr (Excl ()) ∗ R)%I with "[$Ho2 $HR]")=>//.
     iNext. iIntros (lk γlk) "#Hlk".
     wp_let. wp_bind (new_stack _).
     iApply (new_bag_spec N (p_inv' R γm γr))=>//.
diff --git a/theories/logatom/flat_combiner/simple_sync.v b/theories/logatom/flat_combiner/simple_sync.v
index 661f6727ad92aba7c2d6df5ab1b0cd7d9d681792..5d032c8ee5b447f0856f2ccf8f48f563f2667e27 100644
--- a/theories/logatom/flat_combiner/simple_sync.v
+++ b/theories/logatom/flat_combiner/simple_sync.v
@@ -17,13 +17,13 @@ Definition mk_sync: val :=
           "ret".
 
 Section syncer.
-  Context `{!heapG Σ, !lockG Σ} (N: namespace).
+  Context `{!heapG Σ, !lockG Σ}.
   
   Lemma mk_sync_spec: mk_syncer_spec mk_sync.
   Proof.
     iIntros (R Φ) "HR HΦ".
     wp_lam. wp_bind (newlock _).
-    iApply (newlock_spec N R with "[HR]"); first done. iNext.
+    iApply (newlock_spec R with "[HR]"); first done. iNext.
     iIntros (lk γ) "#Hl". wp_pures. iApply "HΦ". iIntros "!#".
     iIntros (f). wp_pures. iAlways.
     iIntros (P Q x) "#Hf !# HP".
diff --git a/theories/logatom/herlihy_wing_queue/hwq.v b/theories/logatom/herlihy_wing_queue/hwq.v
index 115115140a39d9eaf51b16bdb32dc15d88f0e51f..58b66bea4c7455d97c384d03b3188f746f31edb6 100644
--- a/theories/logatom/herlihy_wing_queue/hwq.v
+++ b/theories/logatom/herlihy_wing_queue/hwq.v
@@ -436,7 +436,7 @@ Lemma use_val_wit γs slots i l :
   ⌜val_of <$> slots !! i = Some l⌝.
 Proof.
   iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
-  iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
+  iPureIntro. apply auth_both_valid in H as [H%singleton_included_l _].
   destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
   destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
   inversion_clear H1; rename H into H1.
@@ -466,7 +466,7 @@ Lemma use_name_tok γs slots i γ :
   ⌜name_of <$> slots !! i = Some (Some γ)⌝.
 Proof.
   iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
-  iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
+  iPureIntro. apply auth_both_valid in H as [H%singleton_included_l _].
   destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
   destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
   inversion_clear H1; rename H into H1.
@@ -532,7 +532,7 @@ Lemma use_committed_wit γs slots i :
   ⌜was_committed <$> slots !! i = Some true⌝.
 Proof.
   iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
-  iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
+  iPureIntro. apply auth_both_valid in H as [H%singleton_included_l _].
   destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
   destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
   inversion_clear H1; rename H into H1.
@@ -555,7 +555,7 @@ Lemma use_written_wit γs slots i :
   ⌜was_written <$> slots !! i = Some true⌝.
 Proof.
   iIntros "H● Hwit". iDestruct (own_valid_2 with "H● Hwit") as %H.
-  iPureIntro. apply auth_both_valid in H as [H%singleton_included _].
+  iPureIntro. apply auth_both_valid in H as [H%singleton_included_l _].
   destruct H as [ps (H1 & H2%option_included)]. rewrite lookup_fmap in H1.
   destruct (slots !! i) as [d|]; last by inversion H1. simpl in H1.
   inversion_clear H1; rename H into H1.
@@ -580,7 +580,7 @@ Proof.
   iDestruct (own_valid with "H") as %Hvalid.
   iApply (own_update with "H").
   apply auth_both_valid in Hvalid as [H1 H2].
-  apply singleton_included in H1 as [e (H1_1 & H1_2)].
+  apply singleton_included_l in H1 as [e (H1_1 & H1_2)].
   rewrite lookup_fmap in H1_1.
   destruct (slots !! i) as [[[l s] w]|] eqn:Hi; last by inversion H1_1.
   apply Some_equiv_inj in H1_1.
@@ -611,7 +611,7 @@ Proof.
   iIntros "Hs● Htok". iCombine "Hs● Htok" as "H".
   iDestruct (own_valid with "H") as %Hvalid%auth_both_valid.
   iPureIntro. destruct Hvalid as [H1 H2].
-  apply singleton_included in H1 as [e (H1_1 & H1_2)].
+  apply singleton_included_l in H1 as [e (H1_1 & H1_2)].
   rewrite lookup_fmap in H1_1.
   destruct (slots !! i) as [[[l s] w]|]; last by inversion H1_1.
   apply Some_equiv_inj in H1_1. simpl. f_equal. destruct w; last done.
@@ -641,7 +641,7 @@ Proof.
   rewrite -own_op. iDestruct (own_valid with "H") as %Hvalid.
   iApply (own_update with "H").
   apply auth_both_valid in Hvalid as [H1 H2].
-  apply singleton_included in H1 as [e (H1_1 & H1_2)].
+  apply singleton_included_l in H1 as [e (H1_1 & H1_2)].
   rewrite lookup_fmap in H1_1.
   destruct (slots !! i) as [[[l s] w]|] eqn:Hi; last by inversion H1_1.
   simpl in Hlookup. inversion Hlookup; subst s.
@@ -699,7 +699,7 @@ Proof.
   apply auth_update_core_id; first apply _.
   assert (∃ d, slots !! i = Some d) as [d Hlookup].
   { destruct (slots !! i) as [d|]; inversion H. by exists d. }
-  apply singleton_included. rewrite lookup_fmap. rewrite Hlookup /=.
+  apply singleton_included_l. rewrite lookup_fmap. rewrite Hlookup /=.
   exists (of_slot_data d). split; first done.
   apply Some_included. right. destruct d as [[dl ds] dw]. simpl.
   repeat (apply prod_included; split; simpl);
diff --git a/theories/logatom/lib/gc.v b/theories/logatom/lib/gc.v
index 71316cb10639271efd1240207f38c2dcb65d77e8..d5a8f35a0004373fd29de29c958ed1b0a55aa88b 100644
--- a/theories/logatom/lib/gc.v
+++ b/theories/logatom/lib/gc.v
@@ -100,7 +100,7 @@ Section to_gc_map.
   Lemma gc_map_singleton_included gcm l v :
     {[l := Some (Excl v)]} ≼ to_gc_map gcm → gcm !! l = Some v.
   Proof.
-    rewrite singleton_included.
+    rewrite singleton_included_l.
     setoid_rewrite Some_included_total.
     intros (y & Hsome & Hincluded).
     pose proof (lookup_valid_Some _ _ _ (to_gc_map_valid gcm) Hsome) as Hvalid.
@@ -180,7 +180,7 @@ Section gc.
     iDestruct (own_valid with "Hcomb") as %Hvalid.
     iPureIntro.
     apply auth_both_valid in Hvalid as [Hincluded Hvalid]. 
-    setoid_rewrite singleton_included in Hincluded. 
+    setoid_rewrite singleton_included_l in Hincluded.
     destruct Hincluded as (y & Hsome & _).
     eapply lookup_to_gc_map_Some_2.
     by apply leibniz_equiv_iff in Hsome.