From f1e1f8155b552e9359fe60864f46155fca28a81b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 21 Oct 2020 16:17:32 +0200 Subject: Fixes #13235: remove fragile tolerance for degenerate in-hyps clause. Co-Authored-By: Jim Fehrle --- doc/sphinx/proofs/writing-proofs/rewriting.rst | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f3f69a2fdc..3fe9fce8f5 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -274,9 +274,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. exn:: Too few occurrences. :undocumented: - .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences - This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + In the presence of :n:`with`, this applies :tacn:`change` to the + occurrences specified by :n:`@goal_occurrences`. In the + absence of :n:`with`, :n:`@goal_occurrences` is expected to + only list hypotheses (and optionally the conclusion) without + specifying occurrences (i.e. no :n:`at` clause). .. tacv:: now_show @term -- cgit v1.2.3 From 6adbb8b2c055820777721eae9a3409f9067a8d0e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 21 Oct 2020 19:00:03 +0200 Subject: Adding changelog for #13237. --- .../13237-master+fix13235-no-degenerate-in-hyps-clause.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst (limited to 'doc') diff --git a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst new file mode 100644 index 0000000000..bc67fd025a --- /dev/null +++ b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst @@ -0,0 +1,6 @@ +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 `_, + fixes `#13235 `_, + by Hugo Herbelin). -- cgit v1.2.3