diff options
| author | Pierre-Marie Pédrot | 2020-11-20 13:20:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-20 13:20:18 +0100 |
| commit | 04186f83545e3c693976c73d488b36dd4a2b50db (patch) | |
| tree | 7f22af1415d31b515f8ea4ed42e356279d2756f6 /plugins | |
| parent | 1fd6af1ae6d4a46547cdd2bf812ef46e0727138f (diff) | |
| parent | 6adbb8b2c055820777721eae9a3409f9067a8d0e (diff) | |
Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clauses
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index dbacacab4a..072206c39c 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -377,9 +377,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: |