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

Move old note in proof mode docs.

This note is obsolete due to iris/iris!640
parent c3aae082
No related branches found
No related tags found
No related merge requests found
......@@ -332,12 +332,7 @@ _introduction patterns_:
to destruct nested (separating) conjunctions.
- `[ipat1|ipat2]` : disjunction elimination.
- `[]` : false elimination.
- `%H` : move the hypothesis to the pure Coq context, and name it `H`. Support
for the `%H` introduction pattern requires an implementation of the hook
`string_to_ident`. Without an implementation of this hook, the `%H` pattern
will fail. We provide an implementation of the hook using Ltac2, which works
with Coq 8.11 and later, and can be installed with opam; see
[iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
- `%H` : move the hypothesis to the pure Coq context, and name it `H`.
- `%` : move the hypothesis to the pure Coq context (anonymously). Note that if
`%` is followed by an identifier, and not another token, a space is needed
to disambiguate from `%H` above.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment