From 4b0dd0df49496c100cb8590c76e0ba7f178dd4c6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Apr 2016 20:01:29 +0200
Subject: [PATCH] Make compile with Coq 8.5pl1.

---
 algebra/upred_big_op.v         |  5 ++++-
 program_logic/global_functor.v | 10 ++++++----
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index f33d83299..65023fa60 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -111,8 +111,11 @@ Section gmap.
     m1 ≡ m2 → (∀ x k, m1 !! k = Some x → m2 !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
     Π★{map m1} Φ ⊣⊢ Π★{map m2} Ψ.
   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.
+      eauto using equiv_entails, equiv_entails_sym, @lookup_weaken.
   Qed.
 
   Global Instance big_sepM_ne m n :
diff --git a/program_logic/global_functor.v b/program_logic/global_functor.v
index 03219ee21..9b207fcfa 100644
--- a/program_logic/global_functor.v
+++ b/program_logic/global_functor.v
@@ -72,8 +72,9 @@ Arguments gFunctorList.cons _ _%gFunctor.
 
 Notation "[ ]" := gFunctorList.nil (format "[ ]") : gFunctor_scope.
 Notation "[ F ]" := (gFunctorList.cons F gFunctorList.nil) : gFunctor_scope.
-Notation "[ F ; .. ; F' ]" :=
-  (gFunctorList.cons F .. (gFunctorList.cons F' gFunctorList.nil) ..) : gFunctor_scope.
+Notation "[ F1 ; F2 ; .. ; Fn ]" :=
+  (gFunctorList.cons F1 (gFunctorList.cons F2 ..
+    (gFunctorList.cons Fn gFunctorList.nil) ..)) : gFunctor_scope.
 
 Module gFunctors.
   Definition nil : gFunctors := existT 0 (fin_0_inv _).
@@ -92,8 +93,9 @@ End gFunctors.
 notation hiding a more complex type. *)
 Notation "#[ ]" := gFunctors.nil (format "#[ ]").
 Notation "#[ Fs ]" := (gFunctors.app Fs gFunctors.nil).
-Notation "#[ Fs ; .. ; Fs' ]" :=
-  (gFunctors.app Fs .. (gFunctors.app Fs' gFunctors.nil) ..).
+Notation "#[ Fs1 ; Fs2 ; .. ; Fsn ]" :=
+  (gFunctors.app Fs1 (gFunctors.app Fs2 ..
+    (gFunctors.app Fsn gFunctors.nil) ..)).
 
 (** We need another typeclass to identify the *functor* in the Σ. Basing inG on
    the functor breaks badly because Coq is unable to infer the correct
-- 
GitLab