#[projections(primitive=no)](* FIXME: making this primitive leads to strange TC resolution failures later in this file *)
Structurecmra:=Cmra'{
cmra_car:>Type;
cmra_equiv:Equivcmra_car;
...
...
@@ -190,6 +191,7 @@ Record UcmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} :=
mixin_ucmra_pcore_unit:pcoreε≡@{optionA}Someε
}.
#[projections(primitive=no)](* FIXME: making this primitive leads to strange TC resolution failures in view.v *)
Structureucmra:=Ucmra'{
ucmra_car:>Type;
ucmra_equiv:Equivucmra_car;
...
...
@@ -238,6 +240,7 @@ Section ucmra_mixin.
Enducmra_mixin.
(** * Discrete CMRAs *)
#[projections(primitive=no)](* FIXME: making this primitive means we cannot use the projections with eauto any more (see https://github.com/coq/coq/issues/17561) *)