aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorPierre Roux2018-10-20 14:40:23 +0200
committerPierre Roux2019-04-02 00:02:21 +0200
commit552bb5aba750785d8f19aa7b333baa59e9199369 (patch)
treedf349e57ff8c34e2da48d8c786d2466426822511 /kernel/nativecode.mli
parent4dc3d04d0812005f221e88744c587de8ef0f38ee (diff)
Add parsing of decimal constants (e.g., 1.02e+01)
Rather than integers '[0-9]+', numeral constant can now be parsed according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'. This can be used in one of the two following ways: - using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin - using `Numeral Notation` with the type `decimal` added to `Decimal.v` See examples of each use case in the next two commits.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions