From 57c840e06b922782676450f437e3b0b269e7a5ed Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Mar 2016 10:00:59 +0100
Subject: [PATCH] Remove forgotten admit in auth.
---
algebra/auth.v | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/algebra/auth.v b/algebra/auth.v
index 8abc1dede..5a103b231 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -132,9 +132,11 @@ Canonical Structure authR : cmraT := CMRAT auth_cofe_mixin auth_cmra_mixin.
Global Instance auth_cmra_discrete : CMRADiscrete A → CMRADiscrete authR.
Proof.
split; first apply _.
- intros [[] ?]; rewrite /= /cmra_valid /cmra_validN /=
- -?cmra_discrete_included_iff -?cmra_discrete_valid_iff; auto.
-Admitted.
+ intros [[] ?]; rewrite /= /cmra_valid /cmra_validN /=; auto.
+ - setoid_rewrite <-cmra_discrete_included_iff.
+ rewrite -cmra_discrete_valid_iff. tauto.
+ - by rewrite -cmra_discrete_valid_iff.
+Qed.
(** Internalized properties *)
Lemma auth_equivI {M} (x y : auth A) :
--
GitLab