coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-26	Print a warning when parsing non floating-point values.	Pierre Roux
	For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
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-11-01	Parsing primitive float constants	Pierre Roux