diff --git a/algebra/cmra.v b/algebra/cmra.v
index 08117babe892f8415e2de5af006af85c64eb21a0..6d335bb4448afb4285691087d11d2fa10c78f71c 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1,5 +1,7 @@
 From iris.algebra Require Export ofe.
 
+Set Primitive Projections.
+
 Class PCore (A : Type) := pcore : A → option A.
 Instance: Params (@pcore) 2.
 
@@ -67,7 +69,7 @@ Structure cmraT := CMRAT' {
   cmra_validN : ValidN cmra_car;
   cmra_ofe_mixin : OfeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car;
-  _ : Type
+  cmra_car' : Type
 }.
 Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
 Notation CMRAT A m m' := (CMRAT' A m m' A).
@@ -88,6 +90,8 @@ Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
 Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
 Canonical Structure cmra_ofeC.
 
+Unset Primitive Projections.
+
 (** Lifting properties from the mixin *)
 Section cmra_mixin.
   Context {A : cmraT}.
diff --git a/algebra/ofe.v b/algebra/ofe.v
index 9c2178966b33a968abff0ed2c4eb50dd10f88629..3d05911292e5132a335faa06a197a51fc5e8967f 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -10,6 +10,8 @@ From iris.algebra Require Export base.
 *)
 
 (** Unbundeled version *)
+Set Primitive Projections.
+
 Class Dist A := dist : nat → relation A.
 Instance: Params (@dist) 3.
 Notation "x ≡{ n }≡ y" := (dist n x y)
@@ -42,7 +44,7 @@ Structure ofeT := OfeT' {
   ofe_equiv : Equiv ofe_car;
   ofe_dist : Dist ofe_car;
   ofe_mixin : OfeMixin ofe_car;
-  _ : Type
+  ofe_car' : Type
 }.
 Arguments OfeT' _ {_ _} _ _.
 Notation OfeT A m := (OfeT' A m A).
@@ -54,6 +56,8 @@ Arguments ofe_equiv : simpl never.
 Arguments ofe_dist : simpl never.
 Arguments ofe_mixin : simpl never.
 
+Unset Primitive Projections.
+
 (** Lifting properties from the mixin *)
 Section ofe_mixin.
   Context {A : ofeT}.
@@ -339,7 +343,10 @@ Section ofe_fun.
   Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
   Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC :=
     { compl c x := compl (ofe_fun_chain c x) }.
-  Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
+  Next Obligation. intros ? n c.
+                   intro x. (* This fails. *)
+                   hnf. unfold ofe_dist. intro x. (* This works. *)
+                   apply (conv_compl n (ofe_fun_chain c x)). Qed.
 End ofe_fun.
 
 Arguments ofe_funC : clear implicits.
diff --git a/base_logic/double_negation.v b/base_logic/double_negation.v
index 566343342a23d42549d3b8c4161385ae54d83d24..55cc11f5f8c5b9d82711690c5ba7e6b1120196d3 100644
--- a/base_logic/double_negation.v
+++ b/base_logic/double_negation.v
@@ -79,7 +79,7 @@ Lemma nnupd_ownM_updateP x (Φ : M → Prop) :
   x ~~>: Φ → uPred_ownM x =n=> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
 Proof. 
   intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal. 
-  intros n y ? Hown a.
+  intros n y ? Hown. unfold uPred_holds. intros a.
   red; rewrite //= => n' yf ??.
   inversion Hown as (x'&Hequiv).
   edestruct (Hbupd n' (Some (x' â‹… yf))) as (y'&?&?); eauto.
diff --git a/base_logic/upred.v b/base_logic/upred.v
index ac98bdddc617447ec8de647344cce6372a077ca4..a1051b17fb6f8d47795fe4ce3aa75dc0f80705ec 100644
--- a/base_logic/upred.v
+++ b/base_logic/upred.v
@@ -1,5 +1,6 @@
 From iris.algebra Require Export cmra.
 
+Set Primitive Projections.
 Record uPred (M : ucmraT) : Type := IProp {
   uPred_holds :> nat → M → Prop;
   uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
@@ -8,6 +9,7 @@ Record uPred (M : ucmraT) : Type := IProp {
 Arguments uPred_holds {_} _ _ _ : simpl never.
 Add Printing Constructor uPred.
 Instance: Params (@uPred_holds) 3.
+Unset Primitive Projections.
 
 Delimit Scope uPred_scope with I.
 Bind Scope uPred_scope with uPred.