 22 Jul, 2020 1 commit


Tej Chajed authored
Fixes #337.

 21 Jul, 2020 3 commits


Tej Chajed authored
Preserve identifiers in binders where possible, analogous to the support for destructing existentials in !479. Fixes #336.

Robbert Krebbers authored

Tej Chajed authored
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`.

 15 Jul, 2020 1 commit


Ralf Jung authored

 12 Jun, 2020 1 commit


Tej Chajed authored
Fixes #325. Also added a tests for the various `iSpecialize` error cases involving the `[%]` and `[//]` specialization patterns.

 29 May, 2020 2 commits


Gregory Malecha authored
 it doesn't seem to conflict with anything in Ltac

Ralf Jung authored

 28 May, 2020 4 commits


Gregory Malecha authored

Robbert Krebbers authored

Paolo G. Giarrusso authored

Paolo G. Giarrusso authored

 26 May, 2020 1 commit


Ralf Jung authored

 25 May, 2020 1 commit


Ralf Jung authored

 23 May, 2020 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 20 May, 2020 3 commits
 16 May, 2020 1 commit


Tej Chajed authored
Fixes #319

 15 May, 2020 1 commit


Robbert Krebbers authored

 14 May, 2020 1 commit


Ralf Jung authored

 18 Apr, 2020 2 commits
 15 Apr, 2020 1 commit


Paolo G. Giarrusso authored
Fix #302, including their ASCII variants.  Don't use quotes `'` that are not surrounded by spaces.  However, notation `'(⊢@{' PROP } )` prevents parsing `(⊢@{PROP} Q)` using the `⊢@{PROP} Q` notation. To fix that, we force leftfactorization: we add a notation for `'(⊢@{' PROP } Q )`, defined to coincide with '⊢@{' PROP } Q but which can be leftfactored with `( '⊢@{' PROP } )`.  Add left and right operator sections for (bi)entailment  Add tests. Also do all of the above also for ASCII notations, except for operator sections, which seem to require more discussion.

 14 Apr, 2020 3 commits


Ralf Jung authored

Paolo G. Giarrusso authored

Paolo G. Giarrusso authored

 09 Apr, 2020 1 commit


Ralf Jung authored

 07 Apr, 2020 4 commits


Tej Chajed authored

Tej Chajed authored
Fixes #307.

Gregory Malecha authored

Gregory Malecha authored
 all ascii notation is marked "only parsing" so this PR shouldn't change anything for anyone using only unicode notation.  the algorithm for creating an ascii notation is pretty simple.  \ast > *  \triangleright > >  \vee > \/  \wedge > /\  \forall > forall  \exists > exists  \ast > **

 06 Apr, 2020 1 commit


Tej Chajed authored
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/coqstringident) in Coq 8.10. To use it, you must replace intro_patterns.string_to_ident_hook with a real implementation; see https://gitlab.mpisws.org/iris/stringident for a working implementation that works with Coq 8.11 (using Ltac2). The syntax is %H (within a string intro pattern). This is technically backwardsincompatible, because this was previously supported and parsed as % and H separately. To restore the old behavior, separate with a space, eg [% H].

 03 Apr, 2020 1 commit


Robbert Krebbers authored

 31 Mar, 2020 1 commit


Robbert Krebbers authored

 27 Mar, 2020 1 commit


Paolo G. Giarrusso authored

 20 Mar, 2020 1 commit


Robbert Krebbers authored
