Merge pull request #466 from math-comp/fix-warn

remove typechecking warnings
math-comp · Nov 28, 2024 · 2a29a06 · 2a29a06
2 parents c58f776 + 9515dcd
commit 2a29a06
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/tests/unit/close_hole_term.v b/tests/unit/close_hole_term.v
@@ -3,7 +3,7 @@ From elpi Require Import elpi.
 From Coq Require Export Setoid.
 
 Elpi Query HB.instance lp:{{
-    X = app [{{list}}, Y],
+    X = app [{{list}}, Y_],
     % X needs to be typechecked here to get rid of the hole for the type of Y
     coq.typecheck X _ ok,
     abstract-holes.main X Z,

diff --git a/tests/unit/enrich_type.v b/tests/unit/enrich_type.v
@@ -9,19 +9,19 @@ Elpi Query HB.structure lp:{{
 
 Elpi Query HB.structure lp:{{
     saturate-type-constructor {{list}} X,
-    std.assert! (X = app [{{list}}, Y]) "wrong enriched type"
+    std.assert! (X = app [{{list}}, Y_]) "wrong enriched type"
 }}.
 
 Elpi Query HB.structure lp:{{
     Y = (x \ (y \ {{(prod (list lp:x) (list lp:y))}})),
     saturate-type-constructor (Y _ _) X,
-    std.assert! (X = (app [{{prod}}, (app[{{list}},X1]), app[{{list}},C]])) "wrong enriched type"
+    std.assert! (X = (app [{{prod}}, (app[{{list}},X1_]), app[{{list}},C_]])) "wrong enriched type"
 }}.
 
 Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop :=
 inj x y : S (f x) (f y) -> R x y.
 
 Elpi Query HB.structure lp:{{
     saturate-type-constructor {{Inj}} X,
-    std.assert! (X = app [(global (const Inj)), A, B, R, S, F]) "wrong enriched type"
+    std.assert! (X = app [(global (const Inj_)), A_, B_, R_, S_, F_]) "wrong enriched type"
 }}.
diff --git a/tests/unit/mixin_src_has_mixin_instance.v b/tests/unit/mixin_src_has_mixin_instance.v
@@ -13,7 +13,7 @@ HB.instance Definition nat_m2 : m2 nat := m2.Build nat 1.
 
 
 Elpi Query HB.instance lp:{{
-mixin-src->has-mixin-instance (mixin-src {{nat}} M1 {{nat_m1}}) Y,
+mixin-src->has-mixin-instance (mixin-src {{nat}} M1_ {{nat_m1}}) Y,
 Y = has-mixin-instance (cs-gref {{:gref nat}}) {{:gref m1.phant_axioms}} {{:gref nat_m1}}.
 
 }}.
@@ -22,7 +22,7 @@ Section Test.
 Variable X:s1.type.
 
 Elpi Query HB.instance lp:{{
-mixin-src->has-mixin-instance (mixin-src {{list X}} M1 {{i1 X}}) Y,
+mixin-src->has-mixin-instance (mixin-src {{list X}} M1_ {{i1 X}}) Y,
 Y = has-mixin-instance (cs-gref {{:gref list}}) {{:gref m1.phant_axioms}} {{:gref i1}}.
 
 }}.

diff --git a/tests/unit/struct.v b/tests/unit/struct.v
@@ -8,7 +8,7 @@ HB.structure Definition foo1 := { A of is_foo (option nat) A & m1 A}.
 
 
 Elpi Query HB.structure lp:{{
-std.findall (has-mixin-instance _ _ _) H
+std.findall (has-mixin-instance _ _ _) H_
 }}.
 
 (* here we don't have any declared instances but a clause is still created by the system  :