Skip to content

Commit 33a7b24

Browse files
authored
Merge pull request #71 from vbgl/firstorder-leaf
Explicit which hint database to use with “firstorder” (needed by rocq-prover/rocq#11760)
2 parents 13b19bb + 6053124 commit 33a7b24

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

tests/Test.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1261,7 +1261,7 @@ End Fold_Right_Recursor.
12611261
inversion H.
12621262
firstorder.
12631263
destruct (orb_prop _ _ H1); firstorder.
1264-
firstorder.
1264+
firstorder auto with bool.
12651265
subst.
12661266
rewrite H2; auto.
12671267
Qed.

0 commit comments

Comments
 (0)