Skip to content

Better handling of `let` bindings in proof mode

Robbert Krebbers requested to merge robbert/issue520 into master
  • Make sure that iStartProof fails with a proper error message on goals with let. These lets should either be simpled or introduced into the Coq context.
  • Normalize statements before iIntoValid. This makes sure that iApply works reliable when the lemma statement involves a let.

This fixes #520 (closed).

The MR includes some test cases.

Edited by Ralf Jung

Merge request reports