From e6f6758c3c21964d2f536bf795036b7ae0215358 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Jul 2019 11:20:07 +0200
Subject: [PATCH] tweak proof to also work after a Coq bugfix

---
 theories/algebra/ufrac_auth.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/algebra/ufrac_auth.v b/theories/algebra/ufrac_auth.v
index 99aa1c5d2..d7c1e89ea 100644
--- a/theories/algebra/ufrac_auth.v
+++ b/theories/algebra/ufrac_auth.v
@@ -74,7 +74,7 @@ Section ufrac_auth.
   Proof.
     rewrite auth_both_validN=> -[Hincl Hvalid].
     move: Hincl=> /Some_includedN=> -[[_ ? //]|[[[p' ?] ?] [/=]]].
-    move=> /discrete_iff /leibniz_equiv_iff; rewrite ufrac_op'=> [/Qp_eq/=].
+    rewrite -discrete_iff leibniz_equiv_iff. rewrite ufrac_op'=> [/Qp_eq/=].
     rewrite -{1}(Qcplus_0_r p)=> /(inj (Qcplus p))=> ?; by subst.
   Qed.
   Lemma ufrac_auth_agree p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a ≡ b.
-- 
GitLab