Adapt to coq/coq#17497 (argument renaming more consistently applied)

This seems to be the easiest way to get a backwards compatible fix.
jwiegley · Apr 19, 2023 · fbce036 · fbce036
1 parent 5376e32
commit fbce036
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Lib/NETList.v b/Lib/NETList.v
@@ -19,7 +19,7 @@ Inductive netlist {A : Type} (B : A → A → Type) : A → A → Type :=
 Derive Signature NoConfusion NoConfusionHom Subterm for netlist.
 
 Arguments tfin {A B i j} x.
-Arguments tadd {A B i} j {k} x xs.
+Arguments tadd {A B i} j {k} _ _.
 
 Notation "x :::: xs" := (tadd _ x xs) (at level 60, right associativity).
 

diff --git a/Lib/TList.v b/Lib/TList.v
@@ -35,7 +35,7 @@ Next Obligation.
 Defined.
 
 Arguments tnil {A B i}.
-Arguments tcons {A B i} j {k} x xs.
+Arguments tcons {A B i} j {k} _ _.
 
 Notation "x ::: xs" := (tcons _ x xs) (at level 60, right associativity).