diff options
| author | Hugo Herbelin | 2020-01-31 13:36:34 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-22 15:02:43 +0100 |
| commit | 08189431706298d599cffea2e41dd51290305ba3 (patch) | |
| tree | 919eaba259e65658dc1cda1615250222bac08e9a /interp/notation.mli | |
| parent | 2a31e23df8ff0ab67a09008858fa49e77e5f4332 (diff) | |
Centralizing all kinds of numeral string management in numTok.ml.
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
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 8fcf9dc5dc..892eba8d11 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -81,7 +81,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_numeral +type rawnum = NumTok.Signed.t (** The unique id string below will be used to refer to a particular registered interpreter/uninterpreter of numeral or string notation. @@ -116,8 +116,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t type numnot_option = | Nop - | Warning of string - | Abstract of string + | Warning of NumTok.UnsignedNat.t + | Abstract of NumTok.UnsignedNat.t type int_ty = { uint : Names.inductive; |