diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v index 9858c033cfe68790af779907db849130f86e06ae..54f32f720a24ae8bb6df8fb08a9e5f7103af706d 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -76,6 +76,7 @@ Structure cmraT := CmraT' { cmra_validN : ValidN cmra_car; cmra_ofe_mixin : OfeMixin cmra_car; cmra_mixin : CmraMixin cmra_car; + (* always same as [cmra_car], but by also having this as last field unification sometimes gets faster *) _ : Type }. Arguments CmraT' _ {_ _ _ _ _ _} _ _ _.