Open
Description
Since Stdlib2 will also mean rethinking the hint databases, what about setting the Loose Hint Behavior
option to "Strict"? cc rocq-prover/rocq#7710
Metadata
Metadata
Assignees
Labels
No labels
8000
Since Stdlib2 will also mean rethinking the hint databases, what about setting the Loose Hint Behavior
option to "Strict"? cc rocq-prover/rocq#7710