diff options
| author | Hugo Herbelin | 2020-10-21 16:17:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-17 07:36:01 +0100 |
| commit | f1e1f8155b552e9359fe60864f46155fca28a81b (patch) | |
| tree | cdbbd36a579782bca099a210d4071c07063a808a | |
| parent | 04b25a7635e796ad05ef7db537883594a5144a56 (diff) | |
Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 8 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 6 |
2 files changed, 10 insertions, 4 deletions
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 diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 236de65462..4b2d31ae4a 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -379,9 +379,11 @@ GRAMMAR EXTEND Gram { {onhyps=None; concl_occs=occs} } | "*"; "|-"; occs=concl_occ -> { {onhyps=None; concl_occs=occs} } - | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> + | "|-"; occs=concl_occ -> + { {onhyps=Some []; concl_occs=occs} } + | hl = LIST1 hypident_occ SEP ","; "|-"; occs=concl_occ -> { {onhyps=Some hl; concl_occs=occs} } - | hl=LIST0 hypident_occ SEP"," -> + | hl = LIST1 hypident_occ SEP "," -> { {onhyps=Some hl; concl_occs=NoOccurrences} } ] ] ; clause_dft_concl: |