Skip to content

make eauto solve `is_Some None` as an assumption

Sanjit Bhatrequested to merge
sanjit/stdpp:is_Some_None into master

Previously, is_Some_None matched on a not head (as seen through Print HintDb core), which prevented it from being applied. Now, it matches on a False head, which widens its use.

Note that I had to change from Hint Resolve to Hint Immediate because otherwise, Rocq would eapply is_Some_None to all False goals.

This fixes #180 (closed). #221 (closed) wanted done to solve these goals, which this PR doesn't do.

Merge request reports