Skip to content
Snippets Groups Projects
Commit d5b00af7 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Apply suggestion to docs/proof_mode.md

parent 34062842
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 1 deletion
docs/proof_mode.md
+ 2
− 1
View file @ d5b00af7
...@@ -235,7 +235,8 @@ _introduction patterns_: ...@@ -235,7 +235,8 @@ _introduction patterns_:
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). Note that if - `%` : 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. `%` is followed by an identifier, and not another token, a space is needed
to disambiguate from `%H` above.
- `->` 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
......
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