aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml4
-rw-r--r--doc/tools/docgram/common.edit_mlg8
-rw-r--r--doc/tools/docgram/fullGrammar10
-rw-r--r--parsing/cLexer.ml8
-rw-r--r--parsing/g_constr.mlg4
-rw-r--r--parsing/g_prim.mlg6
-rw-r--r--parsing/pcoq.ml2
-rw-r--r--parsing/tok.ml22
-rw-r--r--parsing/tok.mli4
-rw-r--r--plugins/ssr/ssrparser.mlg8
10 files changed, 38 insertions, 38 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 2735c5b5eb..5e3199e8a6 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -201,8 +201,8 @@ function
| "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s
| "PATTERNIDENT", s -> fprintf fmt "Tok.PPATTERNIDENT (%a)" print_pat s
| "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s
-| "NUMERAL", None -> fprintf fmt "Tok.PNUMERAL None"
-| "NUMERAL", Some s -> fprintf fmt "Tok.PNUMERAL (Some (NumTok.Unsigned.of_string %a))" print_string s
+| "NUMBER", None -> fprintf fmt "Tok.PNUMBER None"
+| "NUMBER", Some s -> fprintf fmt "Tok.PNUMBER (Some (NumTok.Unsigned.of_string %a))" print_string s
| "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s
| "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK"
| "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s
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: [
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
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 60af804c1b..98439e27a1 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -219,20 +219,20 @@ let test_ssrslashnum b1 b2 _ strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "/" ->
(match Util.stream_nth 1 strm with
- | Tok.NUMERAL _ when b1 ->
+ | Tok.NUMBER _ when b1 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
| Tok.KEYWORD "/" ->
if not b2 then () else begin
match Util.stream_nth 3 strm with
- | Tok.NUMERAL _ -> ()
+ | Tok.NUMBER _ -> ()
| _ -> raise Stream.Failure
end
| _ -> raise Stream.Failure)
| Tok.KEYWORD "/" when not b1 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" when not b2 -> ()
- | Tok.NUMERAL _ when b2 ->
+ | Tok.NUMBER _ when b2 ->
(match Util.stream_nth 3 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
@@ -243,7 +243,7 @@ let test_ssrslashnum b1 b2 _ strm =
| Tok.KEYWORD "//" when not b1 ->
(match Util.stream_nth 1 strm with
| Tok.KEYWORD "=" when not b2 -> ()
- | Tok.NUMERAL _ when b2 ->
+ | Tok.NUMBER _ when b2 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:19:41 +0000