adapt to rocq-prover/rocq#19872 (#150)

Author: Yishuai Li

.github/workflows/docker-action.yml

@@ -19,14 +19,15 @@ jobs:
         image:
           - 'coqorg/coq:8.9'
           - 'coqorg/coq:8.11'
-          - 'coqorg/coq:8.12'
+          - 'coqorg/coq:8.12-ocaml-4.10-flambda'
           - 'coqorg/coq:8.13'
           - 'coqorg/coq:8.14'
           - 'coqorg/coq:8.15'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.18'
           - 'coqorg/coq:8.19'
+          - 'coqorg/coq:8.20'
           - 'coqorg/coq:dev'
       fail-fast: false
     steps:
@@ -37,6 +38,11 @@ jobs:
         with:
           opam_file: 'coq-ext-lib.opam'
           custom_image: ${{ matrix.image }}
+          before_install: |
+            startGroup "Setup and print opam config"
+              opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+              opam config list; opam repo list; opam list
+            endGroup
           after_script: |
             startGroup "Test dependants"
               PINS=$(opam list -s --pinned --columns=package | xargs | tr ' ' ,)
@@ -50,7 +56,7 @@ jobs:
             set -o pipefail  # recommended if the script uses pipes
 
             startGroup "Generate Coqdoc"
-              make -j`nproc` coqdoc
+              make -j`nproc` coqdoc || echo "Failed to generate Coqdoc"
             endGroup
           before_script: |
             startGroup "Workaround permission issue"

coqdocjs

@@ -5,6 +5,7 @@ opam_name: coq-ext-lib
 organization: coq-community
 community: true
 action: true
+ci_extra_dev: true
 ci_test_dependants: true
 submodule: true
 
@@ -34,14 +35,15 @@ supported_coq_versions:
 tested_coq_opam_versions:
   - version: '8.9'
   - version: '8.11'
-  - version: '8.12'
+  - version: '8.12-ocaml-4.10-flambda'
   - version: '8.13'
   - version: '8.14'
   - version: '8.15'
   - version: '8.16'
   - version: '8.17'
   - version: '8.18'
   - version: '8.19'
+  - version: '8.20'
   - version: 'dev'
 
 make_target: theories
@@ -52,7 +54,7 @@ action_appendix: |2-
               set -o pipefail  # recommended if the script uses pipes
 
               startGroup "Generate Coqdoc"
-                make -j`nproc` coqdoc
+                make -j`nproc` coqdoc || echo "Failed to generate Coqdoc"
               endGroup
             before_script: |
               startGroup "Workaround permission issue"
@@ -67,6 +69,7 @@ action_appendix: |2-
           if: ${{ always() }}
           run: sudo chown -R 1001:116 .
         - uses: actions/upload-artifact@v4
+          continue-on-error: true
           with:
             name: coqdoc
             path: html

meta.yml

@@ -10,7 +10,7 @@ Section CoMonadLaws.
   Variable m : Type -> Type.
   Variable C : CoMonad m.
 
-  Class CoMonadLaws : Type :=
+  Class CoMonadLaws :=
     {
       extend_extract: forall (A B:Type),
         extend (B:=A) extract = id ;

theories/Structures/CoMonadLaws.v

@@ -24,7 +24,7 @@ Section foldable.
 
   Variable Add : A -> T -> T -> Prop.
 
-  Class FoldableOk : Type :=
+  Class FoldableOk :=
   { fold_ind : forall m (M : Monoid m) (ML : MonoidLaws M) (P : m -> Prop) f u,
                  P (monoid_unit M) ->
                  (forall x y z,

theories/Structures/Foldable.v

@@ -39,7 +39,7 @@ Section MonadLaws.
   Section with_state.
     Context {S : Type}.
 
-    Class MonadStateLaws  (MS : MonadState S m) : Type :=
+    Class MonadStateLaws  (MS : MonadState S m) :=
     { get_put : bind get put = ret tt :> m unit
     ; put_get : forall x : S,
         bind (put x) (fun _ => get) = bind (put x) (fun _ => ret x) :> m S
@@ -51,7 +51,7 @@ Section MonadLaws.
         bind get (fun _ => aM) = aM
     }.
 
-    Class MonadReaderLaws (MR : MonadReader S m) : Type :=
+    Class MonadReaderLaws (MR : MonadReader S m) :=
     { ask_local : forall f : S -> S,
         local f ask = bind ask (fun x => ret (f x))
     ; local_bind : forall {A B} (aM : m A) (f : S -> S) (g : A -> m B),
@@ -64,7 +64,7 @@ Section MonadLaws.
 
   End with_state.
 
-  Class MonadZeroLaws (MZ : MonadZero m) : Type :=
+  Class MonadZeroLaws (MZ : MonadZero m) :=
   { bind_zero : forall {A B} (f : A -> m B),
       bind mzero f = mzero
   }.

theories/Structures/MonadLaws.v

@@ -13,7 +13,7 @@ Section Monoid.
   ; monoid_unit : S
   }.
 
-  Class MonoidLaws@{} (M : Monoid) : Type :=
+  Class MonoidLaws@{} (M : Monoid) :=
   { monoid_assoc : Associative M.(monoid_plus) eq
   ; monoid_lunit : LeftUnit M.(monoid_plus) M.(monoid_unit) eq
   ; monoid_runit : RightUnit M.(monoid_plus) M.(monoid_unit) eq