diff options
Diffstat (limited to 'interp/numTok.mli')
| -rw-r--r-- | interp/numTok.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/numTok.mli b/interp/numTok.mli index 46223c5faf..0b6a877cbd 100644 --- a/interp/numTok.mli +++ b/interp/numTok.mli @@ -1,7 +1,7 @@ type t = { - int : string; (** \[0-9\]+ *) - frac : string; (** empty or \[0-9\]+ *) - exp : string (** empty or \[eE\]\[+-\]?\[0-9\]+ *) + int : string; (** \[0-9\]\[0-9_\]* *) + frac : string; (** empty or \[0-9_\]+ *) + exp : string (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *) } val equal : t -> t -> bool |