diff options
| author | Pierre Roux | 2018-10-20 15:10:54 +0200 |
|---|---|---|
| committer | Pierre Roux | 2019-04-02 00:02:16 +0200 |
| commit | 4dc3d04d0812005f221e88744c587de8ef0f38ee (patch) | |
| tree | 3d66f0198cc168403ec27fd04ac310a0b5c56b1d | |
| parent | a95aacce6cc32726b494d4cc694da49eae86cf96 (diff) | |
Rename raw_natural_number to raw_numeral
In anticipation of an extension from natural numbers to other numeral
constants.
| -rw-r--r-- | interp/constrexpr.ml | 4 | ||||
| -rw-r--r-- | interp/notation.ml | 6 | ||||
| -rw-r--r-- | interp/notation.mli | 6 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | vernac/egramcoq.ml | 2 |
5 files changed, 10 insertions, 10 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index f3d0888fee..fa19eb8ec4 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -54,10 +54,10 @@ type proj_flag = int option (** [Some n] = proj of the n-th visible argument *) multiple leading zeros, and -0 = +0 *) type sign = SPlus | SMinus -type raw_natural_number = string +type raw_numeral = string type prim_token = - | Numeral of sign * raw_natural_number + | Numeral of sign * raw_numeral | String of string type instance_expr = Glob_term.glob_level list diff --git a/interp/notation.ml b/interp/notation.ml index 2c8f5e3a96..6cb95db364 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -476,7 +476,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) (* Interpreting numbers (not in summary because functional objects) *) type required_module = full_path * string list -type rawnum = Constrexpr.sign * Constrexpr.raw_natural_number +type rawnum = Constrexpr.sign * Constrexpr.raw_numeral type prim_token_uid = string @@ -560,8 +560,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of raw_natural_number - | Abstract of raw_natural_number + | Warning of raw_numeral + | Abstract of raw_numeral type int_ty = { uint : Names.inductive; diff --git a/interp/notation.mli b/interp/notation.mli index 4480f3ff75..5423655229 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -77,7 +77,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name type notation_location = (DirPath.t * DirPath.t) * string type required_module = full_path * string list -type rawnum = Constrexpr.sign * Constrexpr.raw_natural_number +type rawnum = Constrexpr.sign * Constrexpr.raw_numeral (** The unique id string below will be used to refer to a particular registered interpreter/uninterpreter of numeral or string notation. @@ -112,8 +112,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of raw_natural_number - | Abstract of raw_natural_number + | Warning of raw_numeral + | Abstract of raw_numeral type int_ty = { uint : Names.inductive; diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e361f0d00f..b733ff46d4 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -157,7 +157,7 @@ module Prim : val pattern_identref : lident Entry.t val base_ident : Id.t Entry.t val natural : int Entry.t - val bigint : Constrexpr.raw_natural_number Entry.t + val bigint : Constrexpr.raw_numeral Entry.t val integer : int Entry.t val string : string Entry.t val lstring : lstring Entry.t diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index b913bccfa3..01e59bbed6 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -245,7 +245,7 @@ type prod_info = production_level * production_position type (_, _) entry = | TTName : ('self, lname) entry | TTReference : ('self, qualid) entry -| TTBigint : ('self, Constrexpr.raw_natural_number) entry +| TTBigint : ('self, Constrexpr.raw_numeral) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry |