coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-04	Move the cbn reduction to its own file, and simplify the RAKAM accordingly.	Pierre-Marie Pédrot

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-02-20	Adding a printer for GlobEnv in ocamldebug.	Hugo Herbelin

2019-05-14	Add aucontext debug printer	Gaëtan Gilbert

2019-02-18	Remove undefined install_printer ppcumulativity_info	Gaëtan Gilbert

2018-10-23	[build] Refactoring to config lib and ocamldebug tweaks.	Emilio Jesus Gallego Arias
	We make `config` into a properly library. This is more uniform and useful for some clients. This also matches what was done in Dune. Next step would be to push dependencies on `Coq_config` upwards, only the actual toplevel binaries should depend on it. We also remove the stale `camlp5.dbg` and refactor the dbg files a bit, isolating the bits that are specific to the plugin / lib building method used by makefile.