From 9e4c13a35c6e15c44218707c6c1b77ed8bdd6e54 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 30 Jan 2017 08:44:40 +0100
Subject: [PATCH] More coherent name for positiveR.
---
theories/algebra/cmra.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 0db38d070..3f1c99a10 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -960,9 +960,9 @@ Section positive.
- intros ???. apply Pos.add_assoc.
- intros ??. apply Pos.add_comm.
Qed.
- Canonical Structure posR : cmraT := discreteR positive pos_ra_mixin.
+ Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
- Global Instance pos_cmra_discrete : CMRADiscrete posR.
+ Global Instance pos_cmra_discrete : CMRADiscrete positiveR.
Proof. constructor; apply _ || done. Qed.
End positive.
--
GitLab