diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 236de65462..072206c39c 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -234,9 +234,7 @@ GRAMMAR EXTEND Gram ; occs_nums: [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl } - | "-"; n = nat_or_var; nl = LIST0 int_or_var -> - (* have used int_or_var instead of nat_or_var for compatibility *) - { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ] + | "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ] ; occs: [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ] @@ -379,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: |