Adding bignat to parse positive numbers; bigint now includes negative ints.

Warning: in notations, the name "bigint" actually meant "bignat". A
clarification will eventually be needed.

5 files changed, 13 insertions, 8 deletions

diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index e8e802f606..2bc1c11596 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -47,7 +47,7 @@ let test_minus_nat =
 
 GRAMMAR EXTEND Gram
   GLOBAL:
-    bigint natural integer identref name ident var preident
+    bignat bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
     ne_string string lstring pattern_ident pattern_identref by_notation
     smart_global bar_cbrace;
@@ -122,13 +122,16 @@ GRAMMAR EXTEND Gram
     [ [ s = string -> { CAst.make ~loc s } ] ]
   ;
   integer:
-    [ [ i = NUMERAL      -> { my_int_of_string loc (check_int loc i) }
-      | test_minus_nat; "-"; i = NUMERAL -> { - my_int_of_string loc (check_int loc i) } ] ]
+    [ [ i = bigint -> { my_int_of_string loc i } ] ]
   ;
   natural:
-    [ [ i = NUMERAL -> { my_int_of_string loc (check_int loc i) } ] ]
+    [ [ i = bignat -> { my_int_of_string loc i } ] ]
   ;
-  bigint: (* Negative numbers are dealt with elsewhere *)
+  bigint:
+    [ [ i = NUMERAL -> { check_int loc i }
+      | test_minus_nat; "-"; i = NUMERAL -> { check_int loc i } ] ]
+  ;
+  bignat:
     [ [ i = NUMERAL -> { check_int loc i } ] ]
   ;
   bar_cbrace:
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index fe2412fcd7..fccd096d11 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -462,6 +462,7 @@ module Prim =
     let ident = gec_gen "ident"
     let natural = gec_gen "natural"
     let integer = gec_gen "integer"
+    let bignat = Entry.create "Prim.bignat"
     let bigint = Entry.create "Prim.bigint"
     let string = gec_gen "string"
     let lstring = Entry.create "Prim.lstring"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cd97ea20fa..87c7f168ce 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -171,6 +171,7 @@ module Prim :
     val pattern_ident : Id.t Entry.t
     val pattern_identref : lident Entry.t
     val base_ident : Id.t Entry.t
+    val bignat : string Entry.t
     val natural : int Entry.t
     val bigint : string Entry.t
     val integer : int Entry.t
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 49d29e7b63..eccefdf64a 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -29,8 +29,8 @@ let pr_numnot_option = function
 VERNAC ARGUMENT EXTEND numnotoption
   PRINTED BY { pr_numnot_option }
 | [ ] -> { Nop }
-| [ "(" "warning" "after" bigint(waft) ")" ] -> { Warning waft }
-| [ "(" "abstract" "after" bigint(n) ")" ] -> { Abstract n }
+| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning waft }
+| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract n }
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 1d790e7cd2..6f8ee76b33 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -368,7 +368,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTClosedBinderList tkl -> MayRecNo (Alist1sep (Aentry Constr.binder, make_sep_rules tkl))
 | TTName -> MayRecNo (Aentry Prim.name)
 | TTOpenBinderList -> MayRecNo (Aentry Constr.open_binders)
-| TTBigint -> MayRecNo (Aentry Prim.bigint)
+| TTBigint -> MayRecNo (Aentry Prim.bignat)
 | TTReference -> MayRecNo (Aentry Constr.global)
 
 let interp_entry forpat e = match e with