3 files changed, 11 insertions, 11 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a619089cdd..549ace5d13 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -780,8 +780,9 @@ numeral: [
 ]
 
 bigint: [
-| DELETE NUMBER
-| num
+| DELETE bignat
+| REPLACE test_minus_nat "-" bignat
+| WITH OPT "-" bignat
 ]
 
 first_letter: [
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index f82f196b36..73b721702e 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -440,8 +440,8 @@ natural: [
 ]
 
 bigint: [
-| NUMBER
-| test_minus_nat "-" NUMBER
+| bignat
+| test_minus_nat "-" bignat
 ]
 
 bignat: [
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 044758f11a..270662b824 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -23,12 +23,11 @@ let my_int_of_string ?loc s =
   with Failure _ ->
     CErrors.user_err ?loc (Pp.str "This number is too large.")
 
-let my_to_nat_string ?loc ispos s =
+let my_to_nat_string ?loc s =
   match NumTok.Unsigned.to_nat s with
   | Some n -> n
   | None ->
-    let pos = if ispos then "a natural" else "an integer" in
-    CErrors.user_err ?loc Pp.(str "This number is not " ++ str pos ++ str " number.")
+    CErrors.user_err ?loc Pp.(str "This number is not an integer.")
 
 let test_pipe_closedcurly =
   let open Pcoq.Lookahead in
@@ -127,12 +126,12 @@ GRAMMAR EXTEND Gram
     [ [ i = bignat -> { my_int_of_string ~loc i } ] ]
   ;
   bigint:
-    [ [ i = NUMBER -> { my_to_nat_string true ~loc i }
-      | test_minus_nat; "-"; i = NUMBER -> { "-" ^ my_to_nat_string ~loc false i } ] ]
+    [ [ i = bignat -> { i }
+      | test_minus_nat; "-"; i = bignat -> { "-" ^ i } ] ]
   ;
   bignat:
-    [ [ i = NUMBER -> { my_to_nat_string ~loc true i } ] ]
- ;
+    [ [ i = NUMBER -> { my_to_nat_string ~loc i } ] ]
+  ;
   bar_cbrace:
     [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
   ;