From 6ef0253d8cb571f3ff5866785fa7a8b015507951 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 30 Sep 2020 16:23:06 +0200
Subject: [PATCH] Remove anonymous Type fields from camera structures.
These were already removed from the OFE and BI structures, but were left here.
---
theories/algebra/cmra.v | 15 ++++++---------
1 file changed, 6 insertions(+), 9 deletions(-)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 6d0a9041e..e284e59dd 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -76,14 +76,12 @@ 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' _ {_ _ _ _ _ _} _ _ _.
+Arguments CmraT' _ {_ _ _ _ _ _} _ _.
(* Given [m : CmraMixin A], the notation [CmraT A m] provides a smart
constructor, which uses [ofe_mixin_of A] to infer the canonical OFE mixin of
the type [A], so that it does not have to be given manually. *)
-Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m A) (only parsing).
+Notation CmraT A m := (CmraT' A (ofe_mixin_of A%type) m) (only parsing).
Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never.
@@ -202,11 +200,10 @@ Structure ucmraT := UcmraT' {
ucmra_ofe_mixin : OfeMixin ucmra_car;
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
- _ : Type;
}.
-Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _ _.
+Arguments UcmraT' _ {_ _ _ _ _ _ _} _ _ _.
Notation UcmraT A m :=
- (UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m A) (only parsing).
+ (UcmraT' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never.
@@ -222,7 +219,7 @@ Hint Extern 0 (Unit _) => eapply (@ucmra_unit _) : typeclass_instances.
Coercion ucmra_ofeO (A : ucmraT) : ofeT := OfeT A (ucmra_ofe_mixin A).
Canonical Structure ucmra_ofeO.
Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
- CmraT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A) A.
+ CmraT' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A).
Canonical Structure ucmra_cmraR.
(** Lifting properties from the mixin *)
@@ -1016,7 +1013,7 @@ Section discrete.
Qed.
Instance discrete_cmra_discrete :
- CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin A).
+ CmraDiscrete (CmraT' A (discrete_ofe_mixin Heq) discrete_cmra_mixin).
Proof. split. apply _. done. Qed.
End discrete.
--
GitLab