coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Use safe demarshalling in the checker.	Pierre-Marie Pédrot	2017-11-28
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Merge branch 'yet-another-makefile-bigbang' into trunk	Pierre Letouzey	2016-06-01
\|\
\| *	Makefile: restore the use of coqdep_boot for creating .v.d files	Pierre Letouzey	2016-06-01
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\|/
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\
\| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\\|
\| *	Fix order of files in mllib.	Maxime Dénès	2016-01-05
* \|	Factorizing unsafe code by relying on the new Dyn module.	Pierre-Marie Pédrot	2015-12-05
\| *	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-25
* \|	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-23
* \|	Using same code for browsing physical directories in coqtop and coqdep.	Hugo Herbelin	2015-02-16
\| *	Revert "Using same code for browsing physical directories in coqtop and coqdep."	Hugo Herbelin	2015-02-12
\| *	Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)	Hugo Herbelin	2015-02-12
\| *	Capital letter in plugins.	Hugo Herbelin	2015-02-12
\| *	Using same code for browsing physical directories in coqtop and coqdep.	Hugo Herbelin	2015-02-12
\|/
*	STM: encapsulate Pp.message in Feedback.feedback	Carst Tankink	2014-08-04
*	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
*	Moving a Thread.yield in check_interrupt.	Pierre-Marie Pédrot	2014-06-07
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	- Fix comparison of universes.	Matthieu Sozeau	2014-05-06
*	printer for coqchk	Enrico Tassi	2014-04-08
*	Adding a canary library. This canary is imperfect. It allows serialization	Pierre-Marie Pédrot	2014-03-05
*	Added a new module HMap. It works (almost) like Map, except that it expects	Pierre-Marie Pédrot	2014-03-05
*	Adding a CSet module in Coq lib.	Pierre-Marie Pédrot	2014-03-05
*	Ephemeron: marshaling friendly keys	gareuselesinge	2013-10-18
*	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot	2013-09-06
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Fix compilation of coqcheck	gareuselesinge	2013-08-20
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Added a generic notion of hook. Hooks are functions to be set	ppedrot	2013-05-12
*	Uniformizing the [if_warn] flag used for warning printing and put	ppedrot	2013-05-08
*	Checker: vo validation is now done in check.ml (and always)	letouzey	2013-04-15
*	Checker: reified encoding of .vo types in values.ml	letouzey	2013-04-15
*	Fix compilation of coqchk (broken by commit 16268), bis repetita	letouzey	2013-03-13
*	Fix compilation of coqchk (broken by commit 16268)	letouzey	2013-03-13
*	Added exception enrichment. Now one can define additional arbitrary	ppedrot	2013-02-18
*	Added backtrace primitives.	ppedrot	2013-01-28
*	Moving hcons_string to String namespace.	ppedrot	2012-12-14
*	Added a CString module.	ppedrot	2012-11-13
*	Added an Int module with dummy utility functions.	ppedrot	2012-11-08
*	Getting rid of Compat in the checker.	ppedrot	2012-10-04
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	Reusing the Hashset data structure in Hashcons. Hopefully, this should	ppedrot	2012-09-26
*	More cleanup of Util: utf8 aspects moved to a new file unicode.ml	letouzey	2012-09-18
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14