From 625011cf7f7c522cfa197958012147cfcb9206a9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 30 Jul 2019 13:15:46 +0200
Subject: [PATCH] explain weird anonymous type field in CmraT
---
theories/algebra/cmra.v | 1 +
1 file changed, 1 insertion(+)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 9858c033c..54f32f720 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' _ {_ _ _ _ _ _} _ _ _.
--
GitLab