Skip to content

Commit c1b1572

Browse files
committed
fix test
1 parent 7042909 commit c1b1572

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

apps/derive/tests-stdlib/test_derive.v

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -183,7 +183,8 @@ derive.eqbOK.register_axiom T is_T is_T_inhab eqb eqb_correct eqb_refl.
183183

184184
Inductive foo := X : T -> foo.
185185

186-
#[only(eqbOK)] derive foo.
186+
#[only(eqbOK),verbose] derive foo.
187+
188+
Redirect "tmp" Print foo_eqb_OK.
187189

188-
Redirect "tmp" Print is_foo_inhab.
189190
End TestRegister.

0 commit comments

Comments
 (0)