Make iFrame able to accumulate assertions in an evar.

See merge request FP/iris-coq!124

This requires changing the Hint Mode of the [Frame] type class because it should not fail if its parameter is an evar, but instantiate it instead. In order to prevent all the other instances of [Frame] to intantiate this evar themselves, we create a new type class [KnwonFrame], which corresponds to the old behavior.

See the discussion in #163.

Super `iModIntro` tactic that generalizes `iAlways`, `iNext`, `iModIntro`, and more

See merge request FP/iris-coq!121

It now no longer requires the modality to be absorbing by default; it
only should be absorbing when non-affine hypotheses have been cleared.

They are split into:
1- KnownMakeXXX , which only works if the parameter is not an evar. Hence, it will never force this evar to becomes e.g., emp or True.
2- MakeXXX, which works even if this is an evar, but it only has instances that will not instanciate arbitrarilly this evar.

As requested by @jtassaro.

- Better error messages
- Handle more inputs

Repair the plainly modality

See merge request FP/iris-coq!122

Thanks to @jtassaro for reporting.