From 552bb5aba750785d8f19aa7b333baa59e9199369 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 20 Oct 2018 14:40:23 +0200 Subject: 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. --- interp/interp.mllib | 1 + 1 file changed, 1 insertion(+) (limited to 'interp/interp.mllib') diff --git a/interp/interp.mllib b/interp/interp.mllib index 147eaf20dc..1262dbb181 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,4 @@ +NumTok Constrexpr Tactypes Stdarg -- cgit v1.2.3