From 9515dcd6a1dae0d059b92e59ad8439388ce6972f Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Thu, 28 Nov 2024 17:02:18 +0100
Subject: [PATCH] remove typechecking warnings

---
 tests/unit/close_hole_term.v              | 2 +-
 tests/unit/enrich_type.v                  | 6 +++---
 tests/unit/mixin_src_has_mixin_instance.v | 4 ++--
 tests/unit/struct.v                       | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/tests/unit/close_hole_term.v b/tests/unit/close_hole_term.v
index 4b63a08a5..b6f2f6887 100644
--- 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
index 72947365c..a4ae536fe 100644
--- a/tests/unit/enrich_type.v
+++ b/tests/unit/enrich_type.v
@@ -9,13 +9,13 @@ 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 :=
@@ -23,5 +23,5 @@ 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
index 0694875fd..db6705bb6 100644
--- 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
index 16e6afd11..6c6a75f4f 100644
--- 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  :