From b198ab3a574dc79cf3a3da5b2056e899487d426f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Jul 2016 10:41:21 +0200
Subject: [PATCH] Remove forgotten admit in f2c246c6.

Also, I removed the @ from lookup_weaken since the Coq bug we
experienced before somehow disappeared.
---
 algebra/upred_big_op.v | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index ba5c04691..85e2b3346 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -123,13 +123,10 @@ Section gmap.
   Lemma big_sepM_proper Φ Ψ m :
     (∀ k x, m !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
     ([★ map] k ↦ x ∈ m, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m, Ψ k x).
-  Proof. (*
-    (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
-    File "./algebra/upred_big_op.v", line 114, characters 4-131:
-    Anomaly: Uncaught exception Univ.AlreadyDeclared. Please report. *)
-    intros [??] ?; apply (anti_symm (⊢)); apply big_sepM_mono;
-      eauto using equiv_entails, equiv_entails_sym, @lookup_weaken.
-  Qed. *) Admitted.
+  Proof.
+    intros ?; apply (anti_symm (⊢)); apply big_sepM_mono;
+      eauto using equiv_entails, equiv_entails_sym, lookup_weaken.
+  Qed.
 
   Global Instance big_sepM_ne m n :
     Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
-- 
GitLab