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 --- plugins/ltac/g_tactic.mlg | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'plugins') 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: -- cgit v1.2.3