fix tests for 8.17

Author: gares

tests/compress_coe.v.out

@@ -1,4 +1,4 @@
-Datatypes_prod__canonical__compress_coe_D = 
+Datatypes_prod__canonical__compress_coe_D =
 fun D D' : D.type =>
 {|
   D.sort := D.sort D * D.sort D';

tests/hnf.v.out

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

tests/infer.v

@@ -17,7 +17,7 @@ HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : Type) := {
 HB.structure Definition bar A P B := { T of barm A P B T }.
 
 #[skip="8.1[0-5].*"] HB.check (bar.type_ bool nat bool).
-#[skip="8.16.*", fail] HB.check (bar.type_ bool nat bool).
+#[skip="8.1[67].*", fail] HB.check (bar.type_ bool nat bool).
 Print bar.phant_type.
 Print bar.type.
 Check bar.type bool nat bool.