do timing on Coq 8.13.2

.gitlab-ci.yml

@@ -33,23 +33,23 @@ build-coq.dev:
   variables:
     OPAM_PINS: "coq version dev"
 
-build-coq.8.13.1:
+build-coq.8.13.2:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.13.1"
+    OPAM_PINS: "coq version 8.13.2"
+    DENY_WARNINGS: "1"
+  tags:
+  - fp-timing
 
 build-coq.8.12.2:
   <<: *template
   variables:
     OPAM_PINS: "coq version 8.12.2"
-    DENY_WARNINGS: "1"
-  tags:
-  - fp-timing
 
 trigger-iris.timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.12.2   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.13.2   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   tags:
   - fp-timing
   only:

README.md

@@ -6,7 +6,7 @@ Some example verification demonstrating the use of Iris.
 
 This version is known to compile with:
 
- - Coq 8.12.2 / 8.13.1
+ - Coq 8.12.2 / 8.13.2
  - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
  - The coq86-devel branch of [Autosubst](https://github.com/uds-psl/autosubst)
 

theories/cl_logic/bi.v

@@ -112,7 +112,7 @@ Global Instance clProp_affine : BiAffine clPropI | 0.
 Proof. intros P. exact: pure_intro. Qed.
 (* Also add this to the global hint database, otherwise [eauto] won't work for
 many lemmas that have [BiAffine] as a premise. *)
-Hint Immediate clProp_affine : core.
+Global Hint Immediate clProp_affine : core.
 
 Global Instance clProp_plain (P : clProp) : Plain P | 0.
 Proof. done. Qed.