Skip to content

Commit 749f375

Browse files
committed
1 parent 2a10928 commit 749f375

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)