Commit 34062842 authored by Robbert Krebbers's avatar Robbert Krebbers

Remark about space.

parent 7b1c37df
...@@ -234,7 +234,8 @@ _introduction patterns_: ...@@ -234,7 +234,8 @@ _introduction patterns_:
will fail. We provide an implementation of the hook using Ltac2, which works will fail. We provide an implementation of the hook using Ltac2, which works
with Coq 8.11, and can be installed with opam; see with Coq 8.11, and can be installed with opam; see
[iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details. [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
- `%` : move the hypothesis to the pure Coq context (anonymously). - `%` : move the hypothesis to the pure Coq context (anonymously). Note that if
`%` is followed by a string, and not another token, a space is needed.
- `->` and `<-` : rewrite using a pure Coq equality - `->` and `<-` : rewrite using a pure Coq equality
- `# ipat` : move the hypothesis into the intuitionistic context. The tactic - `# ipat` : move the hypothesis into the intuitionistic context. The tactic
will fail if the hypothesis is not intuitionistic. On success, the tactic will will fail if the hypothesis is not intuitionistic. On success, the tactic will
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment