From bb9201b521b2a1671fb28585d4446fdb295b26e5 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 24 Mar 2021 12:17:53 +0100 Subject: [PATCH] Move old note in proof mode docs. This note is obsolete due to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/640 --- docs/proof_mode.md | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/docs/proof_mode.md b/docs/proof_mode.md index b383aed63..255a122f2 100644 --- a/docs/proof_mode.md +++ b/docs/proof_mode.md @@ -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. -- GitLab