Commit 57c840e0 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove forgotten admit in auth.

parent ca56a751
......@@ -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) :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment