From cdb384478118abc8f43f34180f25cac4ecd6c05e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 28 Jun 2016 00:31:35 +0200
Subject: [PATCH] Revert "Counting CMRA" because it is already in cmra.v
 (called natR).

This reverts commit 4c056f5e6d327e6167668753f3bd25603b2be804.
---
 _CoqProject     |  1 -
 algebra/count.v | 21 ---------------------
 2 files changed, 22 deletions(-)
 delete mode 100644 algebra/count.v

diff --git a/_CoqProject b/_CoqProject
index 118a945f6..53a3c0def 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -55,7 +55,6 @@ algebra/upred_tactics.v
 algebra/upred_big_op.v
 algebra/upred_hlist.v
 algebra/frac.v
-algebra/count.v
 algebra/csum.v
 algebra/list.v
 algebra/updates.v
diff --git a/algebra/count.v b/algebra/count.v
deleted file mode 100644
index b9ae12650..000000000
--- a/algebra/count.v
+++ /dev/null
@@ -1,21 +0,0 @@
-From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
-Notation count := nat (only parsing).
-
-Section count.
-Canonical Structure countC := leibnizC count.
-
-Instance count_valid : Valid count := λ _, True.
-Instance count_pcore : PCore count := λ _, None.
-Instance count_op : Op count := λ x y, (x + y)%nat.
-
-Definition count_ra_mixin : RAMixin nat.
-Proof. by split; try apply _. Qed.
-Canonical Structure countR := discreteR count count_ra_mixin.
-End count.
-
-(** Internalized properties *)
-Lemma count_equivI {M} (x y : count) : x ≡ y ⊣⊢ (x = y : uPred M).
-Proof. by uPred.unseal. Qed.
-Lemma count_validI {M} (x : count) : ✓ x ⊣⊢ (True : uPred M).
-Proof. by uPred.unseal. Qed.
-- 
GitLab