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 ++++----
 1 file changed, 4 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 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
-- 
cgit v1.2.3