release 0.7.1 (#144)

* release 0.7.1
affeldt-aist · Oct 25, 2024 · 5f0b2e6 · 5f0b2e6
1 parent af25d2c
commit 5f0b2e6
Show file tree

Hide file tree

Showing 5 changed files with 15 additions and 16 deletions.
diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
@@ -17,8 +17,8 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.20'
       fail-fast: false
     steps:
       - uses: actions/checkout@v2

diff --git a/README.md b/README.md
@@ -26,7 +26,7 @@ in several examples of monadic equational reasoning.
   - Celestine Sauvage
   - Kazunari Tanaka
 - License: [LGPL-2.1-or-later](LICENSE)
-- Compatible Coq versions: Coq 8.18-8.19
+- Compatible Coq versions: Coq 8.19-8.20
 - Additional dependencies:
   - [MathComp ssreflect](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)

diff --git a/coq-monae.opam b/coq-monae.opam
@@ -15,17 +15,17 @@ description: """
 This Coq library contains a hierarchy of monads with their laws used
 in several examples of monadic equational reasoning."""
 
-build: [make "-j%{jobs}%"]
+build: [make "-j%{jobs}%" ]
 install: [make "install_full"]
 depends: [
-  "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
+  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-fingroup" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-algebra" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-solvable" { (>= "2.2.0") | (= "dev")  }
   "coq-mathcomp-field" { (>= "2.2.0") | (= "dev")  }
-  "coq-mathcomp-analysis" { (>= "1.2.0")}
-  "coq-infotheo" { >= "0.7.2"}
+  "coq-mathcomp-analysis" { (>= "1.5.0")}
+  "coq-infotheo" { >= "0.7.3"}
   "coq-paramcoq" { >= "1.1.3" & < "1.2~" }
   "coq-hierarchy-builder" { >= "1.5.0" }
   "coq-equations" { >= "1.3" & < "1.4~" }

diff --git a/meta.yml b/meta.yml
@@ -35,14 +35,14 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.18-8.19
-  opam: '{ (>= "8.18" & < "8.20~") | (= "dev") }'
+  text: Coq 8.19-8.20
+  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
 
 tested_coq_opam_versions:
-- version: '2.2.0-coq-8.18'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.20'
+  repo: 'mathcomp/mathcomp'
 
 dependencies:
 - opam:
@@ -72,12 +72,12 @@ dependencies:
     [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-analysis
-    version: '{ (>= "1.2.0")}'
+    version: '{ (>= "1.5.0")}'
   description: |-
     [MathComp analysis](https://github.com/math-comp/analysis)
 - opam:
     name: coq-infotheo
-    version: '{ >= "0.7.2"}'
+    version: '{ >= "0.7.3"}'
   description: |-
     [Infotheo](https://github.com/affeldt-aist/infotheo)
 - opam:

diff --git a/theories/core/hierarchy.v b/theories/core/hierarchy.v
@@ -45,7 +45,7 @@ From HB Require Import structures.
 (*          plusMonad == preplusMonad + commutativity and idempotence         *)
 (*         altCIMonad == altMonad + commutativity + idempotence               *)
 (*        nondetMonad == failMonad + altMonad                                 *)
-(*      nondetCIMonad == failMOnad + altCIMonad                               *)
+(*      nondetCIMonad == failMonad + altCIMonad                               *)
 (*        exceptMonad == failMonad + catch                                    *)
 (*                                                                            *)
 (* Control monads (wip):                                                      *)
@@ -115,7 +115,6 @@ Reserved Notation "f (o) g" (at level 11).
 Reserved Notation "m >> f" (at level 49).
 Reserved Notation "'fmap' f" (at level 4).
 Reserved Notation "x '[~]' y" (at level 50).
-Reserved Notation "mx <| p |> my" (format "mx  <| p |>  my", at level 49).
 
 Notation "f ~~> g" := (forall A, f A -> g A)
   (at level 51, only parsing) : monae_scope.
@@ -1092,8 +1091,8 @@ HB.mixin Structure isML_universe (ml_type : Type) := {
 #[short(type=ML_universe)]
 HB.structure Definition ML_UNIVERSE := {ml_type of isML_universe ml_type & Equality ml_type}.
 
-HB.mixin Record isMonadTypedStore (MLU : ML_universe) (N : monad) (locT : eqType)
-    (M : UU0 -> UU0) of Monad M := {
+HB.mixin Record isMonadTypedStore (MLU : ML_universe) (N : monad)
+    (locT : eqType) (M : UU0 -> UU0) of Monad M := {
   cnew : forall {T : MLU}, coq_type N T -> M (loc locT T) ;
   cget : forall {T}, loc locT T -> M (coq_type N T) ;
   cput : forall {T}, loc locT T -> coq_type N T -> M unit ;