Paolo G. Giarrusso authored 5 years ago and Robbert Krebbers committed 5 years ago

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.

Joseph Tassarotti authored 5 years ago and Robbert Krebbers committed 5 years ago

Also fixes pre-existing bug in iCombine error messages.

For half of #231.

This is a change enabling backward compatibility.

It now supports the specialization pattern `(H spat1 .. spatn)`, which first
recursively specializes the hypothesis `H` using the specialization patterns
`spat1 .. spatn`.

Thanks to @Blaisorblade for reporting.

pm_reduce just reduces away proof mode terms using cbv; pm_prettify just prettifies user-visible connectors using cbn.
Most uses of pm_default are converted to default to keep the desired reduction behavior.

List literals reduce with a spurious `emp` at the end, which is not pretty.