diff options
| author | Hugo Herbelin | 2020-05-14 21:34:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-14 21:34:17 +0200 |
| commit | 56e23844e80e6d607ad5fa56dfeedcd70e97ee70 (patch) | |
| tree | 403c7b43e73fa4159fd997ca26953098b34e22b5 /doc/sphinx | |
| parent | cc54af3842cbf99f169f7937b0e31f737652bd3a (diff) | |
| parent | b5ecd2e46202f47cfccf305e449bcdd8a6a14a0f (diff) | |
Merge PR #12256: Move the static check of evaluability in unfold tactic to runtime.
Reviewed-by: herbelin
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 127e4c6dbe..ad799fbbcd 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3393,17 +3393,6 @@ the conversion in hypotheses :n:`{+ @ident}`. never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to ensure that unfolding does not fail. - .. note:: - - 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 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 - <https://github.com/coq/coq/issues/12179>`_. - .. example:: .. coqtop:: all reset abort @@ -3411,8 +3400,7 @@ the conversion in hypotheses :n:`{+ @ident}`. Opaque id. Goal id 10 = 10. Fail unfold id. - Fail with_strategy transparent [id] unfold id. - let id' := id in with_strategy transparent [id] unfold id'. + with_strategy transparent [id] unfold id. .. warning:: |