From adff7277ef2ba08802d355304b5fa358a0152ab6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Apr 2020 18:37:00 -0400 Subject: [with_strategy] Work around #12191 --- doc/sphinx/proof-engine/tactics.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fa45e10104..7483ab3341 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3370,10 +3370,11 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic unfortunately does not yet play well with tactic internalization, resulting in interpretation-time errors when you try to use it directly with opaque identifiers, as seen in - the following example. This can be worked around by binding the + the first (failing) use of :tacn:`with_strategy` in the + following example. This can be worked around by binding the identifier to an |Ltac| variable, and this issue should - disappear in a future version of |Coq|; see - `#12179 `_. + disappear in a future version of |Coq|; see `#12179 + `_. .. example:: @@ -3382,7 +3383,6 @@ the conversion in hypotheses :n:`{+ @ident}`. Opaque id. Goal id 10 = 10. Fail unfold id. - (** This should work, but does not *) Fail with_strategy transparent [id] unfold id. let id' := id in with_strategy transparent [id] unfold id'. -- cgit v1.2.3