Commit 4b0dd0df authored by Robbert Krebbers's avatar Robbert Krebbers

Make compile with Coq 8.5pl1.

parent e3c56f9e
Pipeline #477 failed with stage
...@@ -111,8 +111,11 @@ Section gmap. ...@@ -111,8 +111,11 @@ Section gmap.
m1 m2 ( x k, m1 !! k = Some x m2 !! k = Some x Φ k x Ψ k x) m1 m2 ( x k, m1 !! k = Some x m2 !! k = Some x Φ k x Ψ k x)
Π★{map m1} Φ Π★{map m2} Ψ. Π★{map m1} Φ Π★{map m2} Ψ.
Proof. 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; 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. Qed.
Global Instance big_sepM_ne m n : Global Instance big_sepM_ne m n :
......
...@@ -72,8 +72,9 @@ Arguments gFunctorList.cons _ _%gFunctor. ...@@ -72,8 +72,9 @@ Arguments gFunctorList.cons _ _%gFunctor.
Notation "[ ]" := gFunctorList.nil (format "[ ]") : gFunctor_scope. Notation "[ ]" := gFunctorList.nil (format "[ ]") : gFunctor_scope.
Notation "[ F ]" := (gFunctorList.cons F gFunctorList.nil) : gFunctor_scope. Notation "[ F ]" := (gFunctorList.cons F gFunctorList.nil) : gFunctor_scope.
Notation "[ F ; .. ; F' ]" := Notation "[ F1 ; F2 ; .. ; Fn ]" :=
(gFunctorList.cons F .. (gFunctorList.cons F' gFunctorList.nil) ..) : gFunctor_scope. (gFunctorList.cons F1 (gFunctorList.cons F2 ..
(gFunctorList.cons Fn gFunctorList.nil) ..)) : gFunctor_scope.
Module gFunctors. Module gFunctors.
Definition nil : gFunctors := existT 0 (fin_0_inv _). Definition nil : gFunctors := existT 0 (fin_0_inv _).
...@@ -92,8 +93,9 @@ End gFunctors. ...@@ -92,8 +93,9 @@ End gFunctors.
notation hiding a more complex type. *) notation hiding a more complex type. *)
Notation "#[ ]" := gFunctors.nil (format "#[ ]"). Notation "#[ ]" := gFunctors.nil (format "#[ ]").
Notation "#[ Fs ]" := (gFunctors.app Fs gFunctors.nil). Notation "#[ Fs ]" := (gFunctors.app Fs gFunctors.nil).
Notation "#[ Fs ; .. ; Fs' ]" := Notation "#[ Fs1 ; Fs2 ; .. ; Fsn ]" :=
(gFunctors.app Fs .. (gFunctors.app Fs' gFunctors.nil) ..). (gFunctors.app Fs1 (gFunctors.app Fs2 ..
(gFunctors.app Fsn gFunctors.nil) ..)).
(** We need another typeclass to identify the *functor* in the Σ. Basing inG on (** 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 the functor breaks badly because Coq is unable to infer the correct
......
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