Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

Fixes #337.

Preserve identifiers in binders where possible, analogous to the support
for destructing existentials in !479.

Fixes #336.

Tej Chajed authored 4 years ago and Robbert Krebbers committed 4 years ago

When running `iDestruct "H" as (?) "H"`, use the name of the binder in
"H". For example, if "H" has type `∃ y, Φ y`,  we now use `y` as the
name of the variable after freshening. Previously the name was always
the equivalent of running `fresh H`.

The implementation achieves this by forwarding the desired identifier
name through the `IntoExist` typeclass. Identifiers are serialized in
Gallina by using them as the name of a function of type `ident_name :=
unit -> unit`.

Fixes #325.

Also added a tests for the various `iSpecialize` error cases involving
the `[%]` and `[//]` specialization patterns.

Fixes #307.

Notably this support relies on string to identifier conversion, which
works natively using Ltac2 in Coq 8.11+ and with a plugin
(https://github.com/ppedrot/coq-string-ident) in Coq 8.10. To use it,
you must replace intro_patterns.string_to_ident_hook with a real
implementation; see https://gitlab.mpi-sws.org/iris/string-ident for a
working implementation that works with Coq 8.11 (using Ltac2).

The syntax is %H (within a string intro pattern). This is technically
backwards-incompatible, because this was previously supported and parsed
as % and H separately. To restore the old behavior, separate with a
space, eg [% H].

- The error messages were wrong: the goal needs to be absorbing, not the hypothesis.
- The wrong failure number was used in `iAssumption`, which caused the error not
  to be propagated properly.

Gregory Malecha authored 5 years ago and Robbert Krebbers committed 5 years ago

- remove "odd" comment
- move atomic triples to bi_scope

It was already marked as deprecated in `doc/proof_mode.md`.

- Rename `IPureElim` -> `iPure`, `IAlwaysElim` -> `IIntuitionistic`
- Drop `IAlwaysIntro` (it's just `IModalIntro`).

Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago

Fixes a new warning on Coq 8.12+alpha when implicit annotations are used
in positions where they are ignored.

Tej Chajed authored 5 years ago and Ralf Jung committed 5 years ago

Coq master is stricter about checking for meaningless implicit binders;
see https://github.com/coq/coq/pull/10202.