Skip to content

Conversation

andres-erbsen
Copy link
Collaborator

@andres-erbsen andres-erbsen commented Jun 2, 2025

  • Added changelog.

This behavior has been one of the reasons for the fiat-crypto fork of nsatz. It's been tested decently widely there.

@andres-erbsen andres-erbsen changed the title Use all hypothesis in nsatz, instead of just lowest consecutive recognized ones Use all hypotheses in nsatz, instead of just lowest consecutive recognized ones Jun 2, 2025
@andres-erbsen andres-erbsen changed the title Use all hypotheses in nsatz, instead of just lowest consecutive recognized ones Use all hypotheses in nsatz, instead of just lowest consequtive recognized ones Jun 2, 2025
@andres-erbsen andres-erbsen force-pushed the nsatz-nonconsecutive branch from f8b8577 to f447c00 Compare June 2, 2025 19:52
@andres-erbsen andres-erbsen marked this pull request as ready for review June 2, 2025 19:52
@andres-erbsen andres-erbsen changed the title Use all hypotheses in nsatz, instead of just lowest consequtive recognized ones Use all hypotheses in nsatz, instead of just lowest consecutive recognized ones Jun 3, 2025
@andres-erbsen andres-erbsen merged commit fc25541 into rocq-prover:master Jun 3, 2025
239 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant