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

---
 parsing/cLexer.ml    |  8 ++++----
 parsing/g_constr.mlg |  4 ++--
 parsing/g_prim.mlg   |  6 +++---
 parsing/pcoq.ml      |  2 +-
 parsing/tok.ml       | 22 +++++++++++-----------
 parsing/tok.mli      |  4 ++--
 6 files changed, 23 insertions(+), 23 deletions(-)

(limited to 'parsing')

diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 85640cabba..a98cf3b7de 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -710,7 +710,7 @@ let rec next_token ~diff_mode loc s =
       let n = NumTok.Unsigned.parse s in
       let ep = Stream.count s in
       comment_stop bp;
-      (NUMERAL n, set_loc_pos loc bp ep)
+      (NUMBER n, set_loc_pos loc bp ep)
   | Some '\"' ->
       Stream.junk s;
       let (loc, len) =
@@ -796,8 +796,8 @@ let token_text : type c. c Tok.p -> string = function
   | PKEYWORD t -> "'" ^ t ^ "'"
   | PIDENT None -> "identifier"
   | PIDENT (Some t) -> "'" ^ t ^ "'"
-  | PNUMERAL None -> "numeral"
-  | PNUMERAL (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'"
+  | PNUMBER None -> "numeral"
+  | PNUMBER (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'"
   | PSTRING None -> "string"
   | PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
   | PLEFTQMARK -> "LEFTQMARK"
@@ -891,5 +891,5 @@ let terminal s =
 
 (* Precondition: the input is a numeral (c.f. [NumTok.t]) *)
 let terminal_numeral s = match NumTok.Unsigned.parse_string s with
-  | Some n -> PNUMERAL (Some n)
+  | Some n -> PNUMBER (Some n)
   | None -> failwith "numeral token expected."
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 61317f3ef2..1ec83c496a 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -258,7 +258,7 @@ GRAMMAR EXTEND Gram
   atomic_constr:
     [ [ g = global; i = univ_instance -> { CAst.make ~loc @@ CRef (g,i) }
       | s = sort   -> { CAst.make ~loc @@  CSort s }
-      | n = NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
+      | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPrim (String s) }
       | "_"      -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
       | "?"; "["; id = ident; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id, None) }
@@ -370,7 +370,7 @@ GRAMMAR EXTEND Gram
           | _ -> p }
       | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
         { CAst.make ~loc @@ CPatOr (p::pl) }
-      | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (NumTok.SPlus,n)) }
+      | n = NUMBER-> { CAst.make ~loc @@ CPatPrim (Numeral (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
   ;
   fixannot:
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index cc59b2175b..044758f11a 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -127,11 +127,11 @@ GRAMMAR EXTEND Gram
     [ [ i = bignat -> { my_int_of_string ~loc i } ] ]
   ;
   bigint:
-    [ [ i = NUMERAL -> { my_to_nat_string true ~loc i }
-      | test_minus_nat; "-"; i = NUMERAL -> { "-" ^ my_to_nat_string ~loc false i } ] ]
+    [ [ i = NUMBER -> { my_to_nat_string true ~loc i }
+      | test_minus_nat; "-"; i = NUMBER -> { "-" ^ my_to_nat_string ~loc false i } ] ]
   ;
   bignat:
-    [ [ i = NUMERAL -> { my_to_nat_string ~loc true i } ] ]
+    [ [ i = NUMBER -> { my_to_nat_string ~loc true i } ] ]
  ;
   bar_cbrace:
     [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ]
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 2cc16f85d5..b9853029a0 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -64,7 +64,7 @@ struct
   | _ -> None
 
   let lk_nat tok n strm = match stream_nth n strm with
-  | Tok.NUMERAL p when NumTok.Unsigned.is_nat p -> Some (n + 1)
+  | Tok.NUMBER p when NumTok.Unsigned.is_nat p -> Some (n + 1)
   | _ -> None
 
   let rec lk_list lk_elem n strm =
diff --git a/parsing/tok.ml b/parsing/tok.ml
index b1ceab8822..1ab7847805 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -17,7 +17,7 @@ type 'c p =
   | PPATTERNIDENT : string option -> string p
   | PIDENT : string option -> string p
   | PFIELD : string option -> string p
-  | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
+  | PNUMBER : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
   | PSTRING : string option -> string p
   | PLEFTQMARK : unit p
   | PBULLET : string option -> string p
@@ -30,8 +30,8 @@ let pattern_strings : type c. c p -> string * string option =
   | PPATTERNIDENT s -> "PATTERNIDENT", s
   | PIDENT s -> "IDENT", s
   | PFIELD s -> "FIELD", s
-  | PNUMERAL None -> "NUMERAL", None
-  | PNUMERAL (Some n) -> "NUMERAL", Some (NumTok.Unsigned.sprint n)
+  | PNUMBER None -> "NUMBER", None
+  | PNUMBER (Some n) -> "NUMBER", Some (NumTok.Unsigned.sprint n)
   | PSTRING s -> "STRING", s
   | PLEFTQMARK -> "LEFTQMARK", None
   | PBULLET s -> "BULLET", s
@@ -43,7 +43,7 @@ type t =
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
-  | NUMERAL of NumTok.Unsigned.t
+  | NUMBER of NumTok.Unsigned.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string
@@ -58,8 +58,8 @@ let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option =
   | PPATTERNIDENT s1, PPATTERNIDENT s2 when streq s1 s2 -> Some Util.Refl
   | PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl
   | PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl
-  | PNUMERAL None, PNUMERAL None -> Some Util.Refl
-  | PNUMERAL (Some n1), PNUMERAL (Some n2) when NumTok.Unsigned.equal n1 n2 -> Some Util.Refl
+  | PNUMBER None, PNUMBER None -> Some Util.Refl
+  | PNUMBER (Some n1), PNUMBER (Some n2) when NumTok.Unsigned.equal n1 n2 -> Some Util.Refl
   | PSTRING s1, PSTRING s2 when streq s1 s2 -> Some Util.Refl
   | PLEFTQMARK, PLEFTQMARK -> Some Util.Refl
   | PBULLET s1, PBULLET s2 when streq s1 s2 -> Some Util.Refl
@@ -73,7 +73,7 @@ let equal t1 t2 = match t1, t2 with
 | PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
 | IDENT s1, IDENT s2 -> string_equal s1 s2
 | FIELD s1, FIELD s2 -> string_equal s1 s2
-| NUMERAL n1, NUMERAL n2 -> NumTok.Unsigned.equal n1 n2
+| NUMBER n1, NUMBER n2 -> NumTok.Unsigned.equal n1 n2
 | STRING s1, STRING s2 -> string_equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
 | BULLET s1, BULLET s2 -> string_equal s1 s2
@@ -100,7 +100,7 @@ let extract_string diff_mode = function
     else s
   | PATTERNIDENT s -> s
   | FIELD s -> if diff_mode then "." ^ s else s
-  | NUMERAL n -> NumTok.Unsigned.sprint n
+  | NUMBER n -> NumTok.Unsigned.sprint n
   | LEFTQMARK -> "?"
   | BULLET s -> s
   | QUOTATION(_,s) -> s
@@ -124,15 +124,15 @@ let match_pattern (type c) (p : c p) : t -> c =
   let err () = raise Stream.Failure in
   let seq = string_equal in
   match p with
-  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMERAL n when seq s (NumTok.Unsigned.sprint n) -> s | _ -> err ())
+  | PKEYWORD s -> (function KEYWORD s' when seq s s' -> s' | NUMBER n when seq s (NumTok.Unsigned.sprint n) -> s | _ -> err ())
   | PIDENT None -> (function IDENT s' -> s' | _ -> err ())
   | PIDENT (Some s) -> (function (IDENT s' | KEYWORD s') when seq s s' -> s' | _ -> err ())
   | PPATTERNIDENT None -> (function PATTERNIDENT s -> s | _ -> err ())
   | PPATTERNIDENT (Some s) -> (function PATTERNIDENT s' when seq s s' -> s' | _ -> err ())
   | PFIELD None -> (function FIELD s -> s | _ -> err ())
   | PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ())
-  | PNUMERAL None -> (function NUMERAL s -> s | _ -> err ())
-  | PNUMERAL (Some n) -> let s = NumTok.Unsigned.sprint n in (function NUMERAL n' when s = NumTok.Unsigned.sprint n' -> n' | _ -> err ())
+  | PNUMBER None -> (function NUMBER s -> s | _ -> err ())
+  | PNUMBER (Some n) -> let s = NumTok.Unsigned.sprint n in (function NUMBER n' when s = NumTok.Unsigned.sprint n' -> n' | _ -> err ())
   | PSTRING None -> (function STRING s -> s | _ -> err ())
   | PSTRING (Some s) -> (function STRING s' when seq s s' -> s' | _ -> err ())
   | PLEFTQMARK -> (function LEFTQMARK -> () | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index b556194eb3..5bbb7a0013 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -15,7 +15,7 @@ type 'c p =
   | PPATTERNIDENT : string option -> string p
   | PIDENT : string option -> string p
   | PFIELD : string option -> string p
-  | PNUMERAL : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
+  | PNUMBER : NumTok.Unsigned.t option -> NumTok.Unsigned.t p
   | PSTRING : string option -> string p
   | PLEFTQMARK : unit p
   | PBULLET : string option -> string p
@@ -29,7 +29,7 @@ type t =
   | PATTERNIDENT of string
   | IDENT of string
   | FIELD of string
-  | NUMERAL of NumTok.Unsigned.t
+  | NUMBER of NumTok.Unsigned.t
   | STRING of string
   | LEFTQMARK
   | BULLET of string
-- 
cgit v1.2.3