Skip to content

Commit 07a799d

Browse files
authored
Merge pull request #398 from proux01/coq_18164
Adapt ro rocq-prover/rocq#18164
2 parents 2a10928 + 749f375 commit 07a799d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tests/funclass.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ About id.
1616

1717
Require Import Arith ssreflect.
1818

19-
HB.instance Definition x1 := has_assoc.Build nat plus plus_assoc.
19+
HB.instance Definition x1 := has_assoc.Build nat plus Nat.add_assoc.
2020

2121
Lemma plus_O_r x : x + 0 = x. Proof. by rewrite -plus_n_O. Qed.
2222
HB.instance Definition x2 := has_neutral.Build nat plus 0 plus_O_n plus_O_r.

0 commit comments

Comments
 (0)