From 00003b625ed3d5f3f2d79cf38ca6ad08e634432e Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 16 Nov 2020 20:24:09 -0800
Subject: Use only nats for occs_nums rather than ints

---
 plugins/ltac/g_tactic.mlg | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins')

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 } ] ]
-- 
cgit v1.2.3