From b4d11894fd676ec53e4fdf860d32173a778242c5 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 4 Sep 2020 15:02:00 +0200
Subject: [parsing] Rename token NUMERAL to NUMBER

---
 doc/tools/docgram/common.edit_mlg |  8 ++++----
 doc/tools/docgram/fullGrammar     | 10 +++++-----
 2 files changed, 9 insertions(+), 9 deletions(-)

(limited to 'doc')

diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 9971a03894..a619089cdd 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -300,7 +300,7 @@ term_let: [
 
 atomic_constr: [
 | MOVETO qualid_annotated global univ_instance
-| MOVETO primitive_notations NUMERAL
+| MOVETO primitive_notations NUMBER
 | MOVETO primitive_notations string
 | MOVETO term_evar "_"
 | REPLACE "?" "[" ident "]"
@@ -780,7 +780,7 @@ numeral: [
 ]
 
 bigint: [
-| DELETE NUMERAL
+| DELETE NUMBER
 | num
 ]
 
@@ -797,7 +797,7 @@ ident: [
 | first_letter LIST0 subsequent_letter
 ]
 
-NUMERAL: [
+NUMBER: [
 | numeral
 ]
 
@@ -2210,7 +2210,7 @@ SPLICE: [
 | IDENT
 | LEFTQMARK
 | natural
-| NUMERAL
+| NUMBER
 | STRING
 | hyp
 | var
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index f628c86cf1..f82f196b36 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -162,7 +162,7 @@ appl_arg: [
 atomic_constr: [
 | global univ_instance
 | sort
-| NUMERAL
+| NUMBER
 | string
 | "_"
 | "?" "[" ident "]"
@@ -283,7 +283,7 @@ pattern0: [
 | "_"
 | "(" pattern200 ")"
 | "(" pattern200 "|" LIST1 pattern200 SEP "|" ")"
-| NUMERAL
+| NUMBER
 | string
 ]
 
@@ -440,12 +440,12 @@ natural: [
 ]
 
 bigint: [
-| NUMERAL
-| test_minus_nat "-" NUMERAL
+| NUMBER
+| test_minus_nat "-" NUMBER
 ]
 
 bignat: [
-| NUMERAL
+| NUMBER
 ]
 
 bar_cbrace: [
-- 
cgit v1.2.3