coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-07-22	[Extraction] Add support for primitive integers	Vincent Laporte
	The ExtrOCamlInt63 module can be required to map primitives from the Int63 module to their OCaml implementation (module Uint63 from the kernel).
2019-04-01	Several improvements and fixes of Lia	Frédéric Besson
	- Improved reification for Micromega (support for #8764) - Fixes #9268: Do not take universes into account in lia reification Improve #9291 by threading the evar_map during reification. Universes are unified. - Remove (potentially cyclic) dependency over lra for Rle_abs - Towards a complete simplex-based lia fixes #9615 Lia is now exclusively using cutting plane proofs. For this to always work, all the variables need to be positive. Therefore, lia is pre-processing the goal for each variable x it introduces the constraints x = y - z , y>=0 , z >= 0 for some fresh variable y and z. For scalability, nia is currently NOT performing this pre-processing. - Lia is using the FSet library manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4 to work around a "leaked" hint breaking compatibility of eauto
2018-11-07	[doc] also scan plugins/ to build the lirbary index	Enrico Tassi

2012-02-01	Improved synchronisation of stdlib index page with current library state.	herbelin
	- Made generation of index page fail if a file is missing in list or listed but unbound in existing theories - Added a file hidden-files to optionally list library files not to show in the index page (though it is currently empty) - Added directory Unicode (why not to have it after all?) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7