coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-22	Adding support for parsing "+" sig in NumTok.	Hugo Herbelin
	Support in the parser needs yet to be added though.
2020-03-22	Centralizing all kinds of numeral string management in numTok.ml.	Hugo Herbelin
	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.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-04-02	Allow underscores as comments in numeral constants.	Pierre Roux
	The numerals lexed are now [0-9][0-9_]* ([.][0-9_]+)? ([eE][+-]?[0-9][0-9_]*)?
2019-04-02	Add parsing of decimal constants (e.g., 1.02e+01)	Pierre Roux
	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.