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 /interp/notation.mli | |
| parent | a95aacce6cc32726b494d4cc694da49eae86cf96 (diff) | |
Rename raw_natural_number to raw_numeral
In anticipation of an extension from natural numbers to other numeral
constants.
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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; |