From 031cc2ba1a19a06766df85b8693c72f16fa62de6 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Mon, 7 Sep 2020 12:07:23 +0200
Subject: [refman] Explicit integer and natural

As respectively bigint and bignat that fit into an OCaml int.
---
 doc/tools/docgram/common.edit_mlg |  6 ++----
 doc/tools/docgram/orderedGrammar  | 12 ++++++++++--
 2 files changed, 12 insertions(+), 6 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 89009764c8..ea60fa22d6 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -756,8 +756,8 @@ hexnat: [
 | [ "0x" | "0X" ] hexdigit LIST0 [ hexdigit | "_" ]
 ]
 
-natural: [
-| REPLACE bignat
+bignat: [
+| REPLACE NUMBER
 | WITH [ decnat | hexnat ]
 ]
 
@@ -2197,7 +2197,6 @@ ltac2_induction_clause: [
 SPLICE: [
 | clause
 | noedit_mode
-| bigint
 | match_list
 | match_context_list
 | IDENT
@@ -2360,7 +2359,6 @@ SPLICE: [
 | search_queries
 | locatable
 | scope_delimiter
-| bignat
 | one_import_filter_name
 | search_where
 | message_token
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 105bd4668e..8d4e0189e6 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -139,6 +139,14 @@ integer: [
 ]
 
 natural: [
+| bignat
+]
+
+bigint: [
+| OPT "-" bignat
+]
+
+bignat: [
 | [ decnat | hexnat ]
 ]
 
@@ -1291,8 +1299,8 @@ field_mod: [
 ]
 
 numeral_modifier: [
-| "(" "warning" "after" number ")"
-| "(" "abstract" "after" number ")"
+| "(" "warning" "after" bignat ")"
+| "(" "abstract" "after" bignat ")"
 ]
 
 hints_path: [
-- 
cgit v1.2.3