diff options
| author | Jim Fehrle | 2020-11-16 20:24:09 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-11-18 12:14:48 -0800 |
| commit | 00003b625ed3d5f3f2d79cf38ca6ad08e634432e (patch) | |
| tree | efb7599f68adf68be2f6aea86970745ea3ca5341 /plugins/ltac | |
| parent | 04b25a7635e796ad05ef7db537883594a5144a56 (diff) | |
Use only nats for occs_nums rather than ints
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_tactic.mlg | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 236de65462..dbacacab4a 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 } ] ] |