This commit closes issue #192.

This fixes issue #187.

sed -i 's/absolute/objective/g; s/relative/subjective/g; s/Absolute/Objective/g; s/Relative/Subjective/g' $(find ./ -name \*.v)

This closes issue #64.

Now they can also be used to clear/frame the whole pure/persistent/spatial
context.

This fixes issue #81.

- Support for a `//` modifier to close the goal using `done`.
- Support for framing in the `[#]` specialization pattern for
  persistent premises, i.e. `[# $H1 $H2]`
- Add new "auto framing patterns" `[$]`, `[# $]` and `>[$]` that
  will try to solve the premise by framing. Hypothesis that are
  not framed are carried over to the next goal.

Thanks to Janno for spotting this!

There are now two proof mode tactics for dealing with modalities:

- `iModIntro` : introduction of a modality
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality

The behavior of these tactics can be controlled by instances of the `IntroModal`
and `ElimModal` type class. We have declared instances for later, except 0,
basic updates and fancy updates. The tactic `iMod` is flexible enough that it
can also eliminate an updates around a weakest pre, and so forth.

The corresponding introduction patterns of these tactics are `!>` and `>`.

These tactics replace the tactics `iUpdIntro`, `iUpd` and `iTimeless`.

Source of backwards incompatability: the introduction pattern `!>` is used for
introduction of arbitrary modalities. It used to introduce laters by stripping
of a later of each hypotheses.

And also rename the corresponding proof mode tactics.