diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index 85e3733b07638adcf134213bca5023e3140fe818..26736ca1d65759db6fe5ce2fcfd0aef1db7868ed 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -71,7 +71,7 @@ Section cnt_model.
     iPureIntro. revert Hfoo.
     rewrite -auth_frag_op -Some_op -pair_op.
     rewrite auth_frag_valid Some_valid.
-    by intros [_ foo%to_agree_op_inv_L']%pair_valid.
+    by intros [_ foo%to_agree_op_inv_L]%pair_valid.
   Qed.
 
   Lemma cnt_agree_2 γ q n m :
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 567e3b79a50e89cb665a66ccadbaef69fa47359b..73ea975ba054cd7549688330d943b179aada91ae 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -142,7 +142,7 @@ Section mapsto.
     rewrite -pair_op singleton_op right_id -pair_op.
     move=> [_ Hv]. move:Hv => /=.
     rewrite singleton_valid.
-    by move=> [_] /to_agree_op_inv_L' [->].
+    by move=> [_] /to_agree_op_inv_L [->].
   Qed.
 
   Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.