remove long-deprecated cofeT and dec_agree

CHANGELOG.md

@@ -186,6 +186,8 @@ Coq 8.10, 8.11, and 8.12 are newly supported by this release, and Coq 8.7 and
   and can be installed with opam; see
   [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
 * Add `auto` hint for `∗-∗`.
+* Remove the long-deprecated `cofeT` alias (for `ofeT`) and `dec_agree` RA (use
+  `agree` instead).
 
 **Changes in `algebra`:**
 

_CoqProject

@@ -33,7 +33,6 @@ theories/algebra/local_updates.v
 theories/algebra/gset.v
 theories/algebra/gmultiset.v
 theories/algebra/coPset.v
-theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/algebra/ufrac.v
 theories/algebra/namespace_map.v

theories/algebra/deprecated.v

-From iris.algebra Require Import ofe cmra.
-Set Default Proof Using "Type".
-
-Local Set Warnings "-deprecated".
-
-(* Old notation for backwards compatibility. *)
-
-(* Deprecated 2016-11-22. Use ofeT instead. *)
-#[deprecated(note = "Use ofeT instead.")]
-Notation cofeT := ofeT (only parsing).
-
-(* Deprecated 2016-12-09. Use agree instead. *)
-Module dec_agree.
-Local Arguments validN _ _ _ !_ /.
-Local Arguments valid _ _  !_ /.
-Local Arguments op _ _ _ !_ /.
-Local Arguments pcore _ _ !_ /.
-
-(* This is isomorphic to option, but has a very different RA structure. *)
-Inductive dec_agree_ (A : Type) : Type :=
-  | DecAgree : A → dec_agree_ A
-  | DecAgreeBot : dec_agree_ A.
-Arguments DecAgree {_} _.
-Arguments DecAgreeBot {_}.
-Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
-  match x with DecAgree a => Some a | _ => None end.
-#[deprecated(note = "Use agree instead.")]
-Notation dec_agree := dec_agree_.
-
-Section dec_agree.
-Context `{EqDecision A}.
-Implicit Types a b : A.
-Implicit Types x y : dec_agree A.
-
-Instance dec_agree_valid : Valid (dec_agree A) := λ x,
-  if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeO : ofeT := leibnizO (dec_agree A).
-
-Instance dec_agree_op : Op (dec_agree A) := λ x y,
-  match x, y with
-  | DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
-  | _, _ => DecAgreeBot
-  end.
-Instance dec_agree_pcore : PCore (dec_agree A) := Some.
-
-#[deprecated(note = "Use agree instead.")]
-Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
-Proof.
-  apply ra_total_mixin; apply _ || eauto.
-  - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|]; by repeat (simplify_eq/= || case_match).
-  - by intros [?|] [?|] ?.
-Qed.
-
-#[deprecated(note = "Use agree instead.")]
-Canonical Structure dec_agreeR : cmraT :=
-  discreteR (dec_agree A) dec_agree_ra_mixin.
-
-Global Instance dec_agree_cmra_discrete : CmraDiscrete dec_agreeR.
-Proof. apply discrete_cmra_discrete. Qed.
-Global Instance dec_agree_cmra_total : CmraTotal dec_agreeR.
-Proof. intros x. by exists x. Qed.
-
-(* Some properties of this CMRA *)
-Global Instance dec_agree_core_id (x : dec_agreeR) : CoreId x.
-Proof. by constructor. Qed.
-
-#[deprecated(note = "Use agree instead.")]
-Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
-Proof. intros. by rewrite /= decide_False. Qed.
-
-#[deprecated(note = "Use agree instead.")]
-Lemma dec_agree_idemp (x : dec_agree A) : x ⋅ x = x.
-Proof. destruct x; by rewrite /= ?decide_True. Qed.
-
-#[deprecated(note = "Use agree instead.")]
-Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2.
-Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
-
-#[deprecated(note = "Use agree instead.")]
-Lemma DecAgree_included a b : DecAgree a ≼ DecAgree b ↔ a = b.
-Proof.
-  split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
-Qed.
-End dec_agree.
-
-Arguments dec_agreeO : clear implicits.
-Arguments dec_agreeR _ {_}.
-End dec_agree.