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 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'doc/tools/docgram/common.edit_mlg')

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