GitLab

We may want to do the same for iIntros ? and iDestruct "H" as {?} "H",
but that requires more work. However, I do not think I want to rely on
names chosen this way.

We now give frame_here priority 0, so it is used immediately when an
evar occurs. This thus avoids loops in the presence of evars.

iSpecialize and iDestruct.

These tactics now all take an iTrm, which is a tuple consisting of
a.) a lemma or name of a hypotheses b.) arguments to instantiate
c.) a specialization pattern.

These tactics are superfluous:
- iPure H as pat => iDestruct H as pat
- iPersistent H => iSpecialize H "!"

It is no longer triggered when posing [P ⊢ Q] with [P] an evar. This, for
example, makes sure that iApply pvs_intro works, which failed before.

This reverts commit 327acdbd. I thought we could
get something with a contractive "un-injection" funtion, but that turns out to
be impossible.

Now, it bases the type the quantifier ranges over on the goal, instead
of the witness. This works better when dealing with witnesses involving
type class constraints.