Merge pull request #398 from proux01/coq_18164

Adapt ro coq/coq#18164
math-comp · Nov 3, 2023 · 07a799d · 07a799d
2 parents 2a10928 + 749f375
commit 07a799d
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tests/funclass.v b/tests/funclass.v
@@ -16,7 +16,7 @@ About id.
 
 Require Import Arith ssreflect.
 
-HB.instance Definition x1 := has_assoc.Build nat plus plus_assoc.
+HB.instance Definition x1 := has_assoc.Build nat plus Nat.add_assoc.
 
 Lemma plus_O_r x : x + 0 = x. Proof. by rewrite -plus_n_O. Qed.
 HB.instance Definition x2 := has_neutral.Build nat plus 0 plus_O_n plus_O_r.