From ec14db89d7fd580904cfa14665c16e877924b8cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 May 2020 10:17:27 +0200 Subject: Remove an outdated piece of documentation about limitations of unfold. --- doc/sphinx/proof-engine/tactics.rst | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) (limited to 'doc') 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 - `_. - .. 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:: -- cgit v1.2.3 From b5ecd2e46202f47cfccf305e449bcdd8a6a14a0f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 14 May 2020 12:37:12 +0200 Subject: Adding changelog. --- doc/changelog/04-tactics/12256-unfold-dyn-check.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/04-tactics/12256-unfold-dyn-check.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/12256-unfold-dyn-check.rst b/doc/changelog/04-tactics/12256-unfold-dyn-check.rst new file mode 100644 index 0000000000..c2f7065f4c --- /dev/null +++ b/doc/changelog/04-tactics/12256-unfold-dyn-check.rst @@ -0,0 +1,4 @@ +- **Changed:** + The check that unfold arguments were indeed unfoldable has been moved to runtime + (`#12256 `_, + by Pierre-Marie Pédrot). -- cgit v1.2.3