diff --git a/algebra/cmra.v b/algebra/cmra.v
index 94d4e370a54e60fea70a9eb3ccd51a60e55f1b7b..64e5e1456a225c279031f3870f1cb886326eea86 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -63,7 +63,7 @@ Structure cmraT := CMRAT' {
   cmra_validN : ValidN cmra_car;
   cmra_cofe_mixin : CofeMixin cmra_car;
   cmra_mixin : CMRAMixin cmra_car;
-  cmra_car' : Type
+  _ : Type
 }.
 Arguments CMRAT' _ {_ _ _ _ _ _ _} _ _ _.
 Notation CMRAT A m m' := (CMRAT' A m m' A).
@@ -165,7 +165,7 @@ Structure ucmraT := UCMRAT' {
   ucmra_cofe_mixin : CofeMixin ucmra_car;
   ucmra_cmra_mixin : CMRAMixin ucmra_car;
   ucmra_mixin : UCMRAMixin ucmra_car;
-  ucmra_car' : Type;
+  _ : Type;
 }.
 Arguments UCMRAT' _ {_ _ _ _ _ _ _ _} _ _ _ _.
 Notation UCMRAT A m m' m'' := (UCMRAT' A m m' m'' A).
diff --git a/algebra/cofe.v b/algebra/cofe.v
index 96ac25d19f45dac3d656b97f6c01be78e23234d5..193e2103caf67227cbb4306933560b3666319b6e 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -64,7 +64,7 @@ Structure cofeT := CofeT' {
   cofe_dist : Dist cofe_car;
   cofe_compl : Compl cofe_car;
   cofe_mixin : CofeMixin cofe_car;
-  cofe_car' : Type
+  _ : Type
 }.
 Arguments CofeT' _ {_ _ _} _ _.
 Notation CofeT A m := (CofeT' A m A).