This was a noop and will soon be an error (until `Inductive` properly
supports locality attributes). See https://github.com/coq/coq/pull/9410

This is in preparation for coq/coq#9274.

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

The continuation is called with a Boolean indicating whether the
hypothesis was in the intuitionistic context or not.

Split it up into more logical parts.

- More consistent indentation.
- Mark new subgoals as comments.

Thanks to @Blaisorblade for reporting.

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

After Coq PR #7825 this will create unwanted evars.

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.

make pm_maybe_wand a BI connective; reduce BI connectives and option combinators in the proofmode with cbn