diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-12 12:15:54 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-12 12:15:54 -0600 |
| commit | a19e20cd3049134b15dbdcf7854a8854a77ccc43 (patch) | |
| tree | 81fced96b49a3d64e390b7cf6f108ea9d0f4e58b /contrib | |
| parent | 3b79066c39054efb95fdb71c3727482764e8a064 (diff) | |
(proof-new) Separate explanation stages in proof equality engine (#5356)
This fixes potential cycles in assertLemma commands in the proof equality engine by using separate proof data structures for the topmost 2 stages of proof generation for equality engine proofs. This fix is required to support datatype proofs for lemmas.
This PR also removes support for the ProofStepBuffer interface in ProofEqEngine, since it is unused, and suffers similar issues and would require a different unique fix.
Diffstat (limited to 'contrib')
0 files changed, 0 insertions, 0 deletions