This fixes issue #67.

It now copies the hypothesis when: 1.) it is persistent 2.) when destructing
it requires a universal quantifier to be instantiated. The new behavior is
implemented using a type class (called CopyDestruct) so that it can easily be
extended.

This fixes issue #51.

This fixes issue #62.

The error message accidentally got removed in e0789039.

This fixes issue #61.

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

For iApply and iRewrite we want that, but for iDestruct and iMod we do not.

This fixes issue #52.

I also renamed `iProof` into `iStartProof`, as it is supposed to be
something internal, and not a substitute of Coq's `Proof` command (as
originally intended).

This fixes issue #44.

    The idea on magic wand is to use it for curried lemmas and use ⊢ for uncurried lemmas.

This way we avoid the env_cbv tactic unfolding string related stuff
that appears in the goal and hypotheses of the proof mode.

The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk *
was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was
a random choice from a unicode chart.

The new symbol ∗ (as proposed by David Swasey) corresponds better to
conventional practise and matches the symbol we use on paper.

Since env_cbv does not unfold these apps, we should do it ourselves,
to avoid ending up with partially evaluated terms.

This fixes issue 39.