• 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
..
algebra.ref Loading commit data...
algebra.v Loading commit data...
atomic.ref Loading commit data...
atomic.v Loading commit data...
heap_lang.ref Loading commit data...
heap_lang.v Loading commit data...
heap_lang2.ref Loading commit data...
heap_lang2.v Loading commit data...
heap_lang_proph.ref Loading commit data...
heap_lang_proph.v Loading commit data...
ipm_paper.ref Loading commit data...
ipm_paper.v Loading commit data...
list_reverse.8.9.ref Loading commit data...
list_reverse.ref Loading commit data...
list_reverse.v Loading commit data...
mosel_paper.ref Loading commit data...
mosel_paper.v Loading commit data...
one_shot.ref Loading commit data...
one_shot.v Loading commit data...
one_shot_once.ref Loading commit data...
one_shot_once.v Loading commit data...
proofmode.ref Loading commit data...
proofmode.v Loading commit data...
proofmode_iris.ref Loading commit data...
proofmode_iris.v Loading commit data...
proofmode_monpred.ref Loading commit data...
proofmode_monpred.v Loading commit data...
telescopes.ref Loading commit data...
telescopes.v Loading commit data...
tree_sum.ref Loading commit data...
tree_sum.v Loading commit data...