This reverts commit daaabf41.  We have tests for
testcase, we shouldn't depend on using arcane features in our definitions for
this purpose.  Also, this exposes that there still is a bug somewhere (see the
FIXME).

We do this in two ways:

- Use `notypeclasses refine` instead of `eapply`, to avoid type class
  search being called arbitrary.
- Use `typeclasses eauto` instead of `apply _`, to avoid type class
  search being called on unrelated evars.

I mainly tried this for `iSpecialize` and friends; this same remains to
be done for all other tactics.

This commit also makes partial progress w.r.t. issue #135.

This is backwards-compatible; it desugars to a normal application on previous versions

Split [FromAssumption] into three, depending on wheter the parameters are evars. This is to avoid loops in TC search.

Renaming and notations for modalities gen_proofmode

See merge request FP/iris-coq!126

sed -i 's/∀ᵢ/\<obj\>/g; s/∃ᵢ/\<subj\>/g' $(find ./ -name \*.v)

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

Bundle classes for updates, plainly and embeddings

See merge request FP/iris-coq!125

Based on an earlier MR by @jung.

This change is slightly more invasive than expected: in monPred we were
using the embedding before the BI was defined. With the new setup, this
is no longer possible, because in order to make an instance of the
embedding, we need to know that `monPred` is a BI. As such, we define
`emp`, `⌜ _ ⌝` and friends directly in the model of `monPred` and later
prove that they are equal to a version in terms of the embedding.