Store a counter in `Envs`  to assign fresh names with `iFresh`.

See merge request FP/iris-coq!128

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)