GitLab

This reverts commit 78ba9509.

This supports Iris 2 like update modalities, as used in e.g. by @jtassaro.

This commit fixes issue #154.

This commit implements a generic `iAlways` tactic that is not tied to
`persistently`, `affinely` and `plainly` but can be instantiated with a
variety of always-style modalities.

In order to plug in an always-style modality, one has to decide for both
the persistent and spatial what action should be performed upon introducing
the modality:

- Introduction is only allowed when the context is empty.
- Introduction is only allowed when all hypotheses satisfy some predicate
  `C : PROP → Prop` (where `C` should be a type class).
- Introduction will only keep the hypotheses that satisfy some predicate
  `C : PROP → Prop` (where `C` should be a type class).
- Introduction will clear the context.
- Introduction will keep the context as-if.

Formally, these actions correspond to the following inductive type:

```coq
Inductive always_intro_spec (PROP : bi) :=
  | AIEnvIsEmpty
  | AIEnvForall (C : PROP → Prop)
  | AIEnvFilter (C : PROP → Prop)
  | AIEnvClear
  | AIEnvId.
```

An always-style modality is then a record `always_modality` packing together the
modality with the laws it should satisfy to justify the given actions for both
contexts.

1- Avoid [type_term (eq_refl : @eq Type PROP PROP')] when [PROP] is not given. This has significant performance implications.
2- In th case PROP is given (i.e., only when the tactic is manually used), introduce all the foralls and lets.

This used to be done by using `ElimModal` in backwards direction. Having
a separate type class for this gets rid of some hacks:

- Both `Hint Mode`s in forward and backwards direction for `ElimModal`.
- Weird type class precedence hacks to make sure the right instance is picked.
  These were needed because using `ElimModal` in backwards direction caused
  ambiguity.

Use [notypeclasses refine] instead of eapply in iLöb and iNext, to workaround the confusion of apply wrt canonical structures.

It used to be an inline pattern match.

This also restores compatibility with Coq 8.6.1.