Merge pull request #282 from math-comp/ci-8.15

[ci] docker on 8.15
math-comp · Jan 9, 2022 · 9614134 · 9614134
2 parents 14dfa74 + 192dcc2
commit 9614134
Show file tree

Hide file tree

Showing 5 changed files with 42 additions and 1 deletion.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -19,6 +19,7 @@ jobs:
         coq_version:
           - '8.13'
           - '8.14'
+          - '8.15'
         ocaml_version:
           - '4.07-flambda'
     steps:

diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam
@@ -12,7 +12,7 @@ build: [ [ make "build"]
          [ make "test-suite" ] {with-test}
        ]
 install: [ make "install" ]
-depends: [ "coq-elpi" { (>= "1.11.0" & < "1.12~") | = "dev" } ]
+depends: [ "coq-elpi" { (>= "1.11.0" & < "1.13~") | = "dev" } ]
 conflicts: [ "coq-hierarchy-builder-shim" ]
 synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
 description: """

diff --git a/tests/compress_coe.v.out b/tests/compress_coe.v.out
@@ -17,3 +17,5 @@ fun D D' : D.type =>
     |}
 |}
      : D.type -> D.type -> D.type
+
+Arguments Datatypes_prod__canonical__compress_coe_D D D'
diff --git a/tests/compress_coe.v.out.13 b/tests/compress_coe.v.out.13
@@ -0,0 +1,19 @@
+Datatypes_prod__canonical__compress_coe_D = 
+fun D D' : D.type =>
+{|
+  D.sort := D.sort D * D.sort D';
+  D.class :=
+    {|
+      D.compress_coe_hasA_mixin :=
+        prodA (compress_coe_D__to__compress_coe_A D)
+          (compress_coe_D__to__compress_coe_A D');
+      D.compress_coe_hasB_mixin :=
+        prodB tt (compress_coe_D__to__compress_coe_B D)
+          (compress_coe_D__to__compress_coe_B D');
+      D.compress_coe_hasC_mixin :=
+        prodC tt tt (compress_coe_D__to__compress_coe_C D)
+          (compress_coe_D__to__compress_coe_C D');
+      D.compress_coe_hasD_mixin := prodD D D'
+    |}
+|}
+     : D.type -> D.type -> D.type
diff --git a/tests/compress_coe.v.out.14 b/tests/compress_coe.v.out.14
@@ -0,0 +1,19 @@
+Datatypes_prod__canonical__compress_coe_D = 
+fun D D' : D.type =>
+{|
+  D.sort := D.sort D * D.sort D';
+  D.class :=
+    {|
+      D.compress_coe_hasA_mixin :=
+        prodA (compress_coe_D__to__compress_coe_A D)
+          (compress_coe_D__to__compress_coe_A D');
+      D.compress_coe_hasB_mixin :=
+        prodB tt (compress_coe_D__to__compress_coe_B D)
+          (compress_coe_D__to__compress_coe_B D');
+      D.compress_coe_hasC_mixin :=
+        prodC tt tt (compress_coe_D__to__compress_coe_C D)
+          (compress_coe_D__to__compress_coe_C D');
+      D.compress_coe_hasD_mixin := prodD D D'
+    |}
+|}
+     : D.type -> D.type -> D.type