Merge pull request #365 from proux01/fix_ci

[CI] Fix

.nix/config.nix

@@ -15,7 +15,7 @@
       mathcomp-finmap.override.version = "master";
       mathcomp.analyis.override.version = "hierarchy-builder";
       interval.override.version = "master";
-      reglang.override.version = "hierarchy-builder";
+      reglang.override.version = "master";
       coq-bits.override.version = "hierarchy-builder";
       deriving.job = false;
     };

tests/compress_coe.v.out.15

@@ -0,0 +1,21 @@
+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
+
+Arguments Datatypes_prod__canonical__compress_coe_D D D'

tests/compress_coe.v.out.16

@@ -0,0 +1,21 @@
+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
+
+Arguments Datatypes_prod__canonical__compress_coe_D D D'

tests/hnf.v.out.15

@@ -0,0 +1,12 @@
+Datatypes_nat__canonical__hnf_S = 
+{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
+     : S.type
+HB_unnamed_mixin_12 = 
+{| M.x := f.y nat HB_unnamed_factory_10 + 1 |}
+     : M.axioms_ nat
+Datatypes_bool__canonical__hnf_S = 
+{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |}
+     : S.type
+HB_unnamed_mixin_16 = 
+Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13
+     : M.axioms_ bool

tests/hnf.v.out.16

@@ -0,0 +1,12 @@
+Datatypes_nat__canonical__hnf_S = 
+{| S.sort := nat; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_12 |} |}
+     : S.type
+HB_unnamed_mixin_12 = 
+{| M.x := f.y nat HB_unnamed_factory_10 + 1 |}
+     : M.axioms_ nat
+Datatypes_bool__canonical__hnf_S = 
+{| S.sort := bool; S.class := {| S.hnf_M_mixin := HB_unnamed_mixin_16 |} |}
+     : S.type
+HB_unnamed_mixin_16 = 
+Builders_6.HB_unnamed_factory_8 bool HB_unnamed_factory_13
+     : M.axioms_ bool