From 35a17feb96b0f1645648010c1f7218d539096a5b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Dec 2016 12:18:57 +0100
Subject: [PATCH] turns out naming the module dec_agree_deprecated is not
necessary
---
CHANGELOG.md | 3 ++-
theories/algebra/deprecated.v | 7 ++-----
2 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index aa2753d8e..d7eb3f468 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,7 +18,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
recursive domain equation. As a consequence, CMRAs no longer need a proof of
completeness. (The old `cofeT` is provided by `algebra.deprecated`.)
* Implement a new agreement construction. Unlike the old one, this one
- preserves discreteness.
+ preserves discreteness. dec_agree is thus no longer needed and has been moved
+ to algebra.deprecated.
* Renaming and moving things around: uPred and the rest of the base logic are in
`base_logic`, while `program_logic` is for everything involving the general
Iris notion of a language.
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 753d956e7..45024d71d 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -6,10 +6,7 @@ From iris.algebra Require Import ofe cmra.
Notation cofeT := ofeT (only parsing).
(* Deprecated 2016-12-09. Use agree instead. *)
-(* The module is called dec_agree_deprecated because if it was just dec_agree,
- it would still be imported by "From iris Import dec_agree", and people would
- not notice they use sth. deprecated. *)
-Module dec_agree_deprecated.
+Module dec_agree.
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ _ !_ /.
@@ -76,4 +73,4 @@ End dec_agree.
Arguments dec_agreeC : clear implicits.
Arguments dec_agreeR _ {_}.
-End dec_agree_deprecated.
+End dec_agree.
--
GitLab