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.

1 files changed, 2 insertions, 2 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 338ffb706d..60610b92b8 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -50,8 +50,8 @@ let names_of_local_binders bl =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-(* Note: redundant Numeral representations such as -0 and +0 (or different
-   numbers of leading zeros) are considered different here. *)
+(* Note: redundant Numeral representations, such as -0 and +0 (and others),
+   are considered different here. *)
 
 let prim_token_eq t1 t2 = match t1, t2 with
 | Numeral (SPlus,n1), Numeral (SPlus,n2)