• 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 Loading commit data...
base_logic Loading commit data...
bi Loading commit data...
heap_lang Loading commit data...
program_logic Loading commit data...
proofmode Loading commit data...