From aa6c43a2d3087ad4c346fe7e3c7ca8f5c737f9f3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Jun 2016 21:06:36 +0200
Subject: [PATCH] Make additional carrier fields in structures anonymous.
---
algebra/cmra.v | 4 ++--
algebra/cofe.v | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 94d4e370a..64e5e1456 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 96ac25d19..193e2103c 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).
--
GitLab