Skip to content
  • Paolo G. Giarrusso's avatar
    Fix iPoseProof on recursive lemmas (fix #274) · 3f468582
    Paolo G. Giarrusso authored and Robbert Krebbers's avatar Robbert Krebbers committed
    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.