Merge pull request #4 from pPomCo/gha-ITP2023

chore: Update docker-action.yml (ITP2023 branch)
pPomCo · Oct 26, 2023 · 277a1cf · 277a1cf
2 parents 09361d1 + 4d989f9
commit 277a1cf
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 14 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -1,14 +1,14 @@
-# This file was generated from `meta.yml`, please do not edit manually.
+# This file was generated from `meta.yml`, then modified.
 # Follow the instructions on https://github.com/coq-community/templates to regenerate.
 name: Docker CI
 
 on:
   push:
     branches:
-      - main
+      - ITP2023
   pull_request:
     branches:
-      - '**'
+      - ITP2023
 
 jobs:
   build:
@@ -17,9 +17,12 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:1.15.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.18'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.17'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.16'
+          - 'mathcomp/mathcomp:1.17.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.16.0-coq-8.15'
           - 'mathcomp/mathcomp:1.15.0-coq-8.15'
-          - 'mathcomp/mathcomp:1.15.0-coq-8.14'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.15'
       fail-fast: false

diff --git a/README.md b/README.md
@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/pPomCo/belgames/workflows/Docker%20CI/badge.svg?branch=main
-[docker-action-link]: https://github.com/pPomCo/belgames/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/pPomCo/belgames/actions/workflows/docker-action.yml/badge.svg?branch=ITP2023
+[docker-action-link]: https://github.com/pPomCo/belgames/actions/workflows/docker-action.yml
 
 
 

diff --git a/coq-belgames.opam b/coq-belgames.opam
@@ -23,8 +23,8 @@ into games of complete information, i.e., without any uncertainty."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.14" & < "8.17~")}
-  "coq-mathcomp-algebra" {(>= "1.13" & < "1.16~")}
+  "coq" {(>= "8.14" & < "8.19~")}
+  "coq-mathcomp-algebra" {(>= "1.13" & < "1.18~")}
 ]
 
 tags: [

diff --git a/theories/HRtransform.v b/theories/HRtransform.v
@@ -534,8 +534,8 @@ Section HRTBMWeakConditioningLocalGames.
     * by rewrite ffunE (negbTE HX).
   + apply/forallP => X.
     rewrite ffunE.
-    case (boolP (X == setT)) => [->//|H].
-    exact: ler01. by rewrite (negbTE H) //.
+    case (boolP (X == setT)) => [->|H] ;
+      by rewrite ?ler01 // (negbTE H) //.
   Defined.
 
   Definition HRTBM_Weak_example_belgame : belgame R A T :=
@@ -545,7 +545,6 @@ Section HRTBMWeakConditioningLocalGames.
   Proof.
   apply/forallP => i ; apply/forallP => ti.
   rewrite/revisable/Weak_conditioning/Weak_revisable/Pl.
-  Search (_ > 0) (_ != 0).
   apply: lt0r_neq0.
   rewrite (bigD1 setT) /=.
   - rewrite ffunE eqxx big1 => [|X /andP [HX1 HX2]].

diff --git a/theories/bel.v b/theories/bel.v
@@ -1289,7 +1289,7 @@ Section BelOnFFuns.
     exact: proba_set1.
   - apply/forallP => t.
     rewrite ffunE.
-    apply big_ind => // [||i _] ; first by rewrite ler01.
+    apply big_ind ; rewrite ?ler01=>// i Hi.
     apply mulr_ge0.
     have [_ _ Hm3] := and3P (bpa_ax (p i)).
     exact: (forallP Hm3).

diff --git a/theories/general_lemmas.v b/theories/general_lemmas.v
@@ -452,7 +452,7 @@ Section NumLemmas.
   Lemma prod_ge0 {X} (P : pred X) (f : X -> R) :
     (forall x, P x -> f x >= 0) -> \prod_(x | P x) f x >= 0.
   Proof.
-  move => H ; apply big_ind => //= ; first by rewrite ler01.
+  move => H ; apply big_ind ; rewrite ?ler01//.
   exact: mulr_ge0.
   Qed.