1. 22 Jul, 2020 1 commit
  2. 21 Jul, 2020 3 commits
    • Tej Chajed's avatar
      Use user-supplied names in iIntros · c1affb21
      Tej Chajed authored
      Preserve identifiers in binders where possible, analogous to the support
      for destructing existentials in !479.
      
      Fixes #336.
      c1affb21
    • Robbert Krebbers's avatar
      Tweak some names in test file. · 11678073
      Robbert Krebbers authored
      11678073
    • Tej Chajed's avatar
      Use user names when destructing existentials · 7d0bb151
      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`.
      7d0bb151
  3. 15 Jul, 2020 1 commit
  4. 12 Jun, 2020 1 commit
  5. 29 May, 2020 2 commits
  6. 28 May, 2020 4 commits
  7. 26 May, 2020 1 commit
  8. 25 May, 2020 1 commit
  9. 23 May, 2020 4 commits
  10. 20 May, 2020 3 commits
  11. 16 May, 2020 1 commit
  12. 15 May, 2020 1 commit
  13. 14 May, 2020 1 commit
  14. 18 Apr, 2020 2 commits
  15. 15 Apr, 2020 1 commit
    • Paolo G. Giarrusso's avatar
      Fix entailment notations `(⊢@{PROP})` and `(⊣⊢@{PROP} )` etc. · 1b820fbf
      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 left-factorization: we add a notation for `'(⊢@{' PROP }
      Q )`, defined to coincide with '⊢@{' PROP } Q but which can be left-factored
      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.
      1b820fbf
  16. 14 Apr, 2020 3 commits
  17. 09 Apr, 2020 1 commit
  18. 07 Apr, 2020 4 commits
  19. 06 Apr, 2020 1 commit
    • Tej Chajed's avatar
      Add support for pure names in intro patterns · 1375d6aa
      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/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].
      1375d6aa
  20. 03 Apr, 2020 1 commit
  21. 31 Mar, 2020 1 commit
  22. 27 Mar, 2020 1 commit
  23. 20 Mar, 2020 1 commit