• Paolo G. Giarrusso's avatar
    Fix iPoseProof on recursive lemmas (fix #274) · 3f468582
    Paolo G. Giarrusso authored
    When proving `foo` through a fixpoint, Coq's guardedness checker needs to see to
    which arguments `foo` is applied. Opaque lemmas applied to `foo` itself prevent
    that, so make them transparent.
    * Make `IntoEmpValid` lemmas transparent.
    * Expose application of `IntoEmpValid` instance to its argument.
    * Add comment to `tac_pose_proof`
    
    This MR brings back the type of `tac_pose_proof` to the one it had before !329.
    Hence, this seems worth a comment.
    3f468582
Name
Last commit
Last update
.gitlab/issue_templates Loading commit data...
benchmark Loading commit data...
docs Loading commit data...
tests Loading commit data...
tex Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.gitmodules Loading commit data...
CHANGELOG.md Loading commit data...
CONTRIBUTING.md Loading commit data...
LICENSE Loading commit data...
LICENSE-CODE Loading commit data...
LICENSE-DOCS Loading commit data...
Makefile Loading commit data...
Makefile.coq.local Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
build-all Loading commit data...
descr Loading commit data...
opam Loading commit data...
test-normalizer.sed Loading commit data...