coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
*	Declare assumptions of well-founded definitions as unsafe.	Arnaud Spiwack	2015-09-25
*	Propagate `Guarded` flag from syntax to kernel.	Arnaud Spiwack	2015-09-25
*	Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming gua...	Arnaud Spiwack	2015-09-25
*	Add a flag to deactivate guard checking in the kernel.	Arnaud Spiwack	2015-06-26
*	When assuming an inductive type positive, then it is declared "unsafe" to the...	Arnaud Spiwack	2015-06-24
*	Add corresponding field in `VernacInductive`.	Arnaud Spiwack	2015-06-24
*	Add a corresponding field in `mutual_inductive_entry` (part 1).	Arnaud Spiwack	2015-06-24
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\
\| *	improve --help documentation: the -m\|--memory option was missing	Gabriel Scherer	2015-06-24
\| *	when OCAML_GC_STATS points to a filepath, write Gc stats into it	Gabriel Scherer	2015-06-24
\| *	Splitting the library representation on disk in two.	Pierre-Marie Pédrot	2015-06-24
\| *	obligations: wrap Ephemeron.get to make error more informative	Enrico Tassi	2015-06-23
\| *	Wrap the program_info type up in the ephemeron mechanism	Alec Faithfull	2015-06-23
* \|	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-23
\| *	Add a Set Dump Bytecode command for debugging purposes.	Maxime Dénès	2015-06-23
\| *	Warning are enabled by default in interactive mode.	Pierre-Marie Pédrot	2015-06-23
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-06-22
\|\\|
\| *	Remove uses of polymorphic equality from prev. commit	Clément Pit--Claudel	2015-06-22
\| *	Replace 'try ... with Failure "List.last"' with 'if l <> []'	Clément Pit--Claudel	2015-06-22
\| *	Guard the List.hd call in [Show Intros]	Clément Pit--Claudel	2015-06-22
* \|	All invocations to ocaml compilers go through ocamlfind	Pierre Boutillier	2015-06-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-01
\|\\|
\| *	coqtop: reset the current file name after a load-vernac-source	Enrico Tassi	2015-05-29
\| *	Flag -test-mode intended to be used for ad-hoc prints in test-suite	Enrico Tassi	2015-05-29
\| *	make Unset Silent work in coqc	Enrico Tassi	2015-05-29
\| *	Fix bug #4159	Matthieu Sozeau	2015-05-27
\| *	Uncaught exception termination exits coqtop with the anomaly errno.	Pierre-Marie Pédrot	2015-05-18
\| *	The Fail command does not catch uncaught exception anomalies anymore.	Pierre-Marie Pédrot	2015-05-18
\| *	Disabling colors when tERM variable is "dumb".	Pierre Courtieu	2015-05-18
\| *	Fix usage about -color.	Pierre Courtieu	2015-05-18
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	The -list-tag options now prints the corresponding COQ_COLORS value.	Pierre-Marie Pédrot	2015-05-14
\| *	Adding an option -w to control Coq warning output.	Pierre-Marie Pédrot	2015-05-14
\| *	Disable precompilation for native_compute by default.	Guillaume Melquiond	2015-05-14
\| *	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
\| *	Better error message for non-existent required libraries with a From prefix.	Pierre-Marie Pédrot	2015-05-13
\| *	STM: process_error_hook set in Vernac where fname is known (fix #4229)	Enrico Tassi	2015-05-12
\| *	Adding a test to check whether two tactic notations conflict.	Pierre-Marie Pédrot	2015-05-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
\| *	Fixing computation of implicit arguments by position in fixpoints (#4217).	Hugo Herbelin	2015-05-01
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Using tclZEROMSG instead of tclZERO in several places.	Pierre-Marie Pédrot	2015-04-23
\| *	No longer add dev/ to the LoadPath, only to the ML path.	Guillaume Melquiond	2015-04-17
\| *	Fixing bug #4190.	Pierre-Marie Pédrot	2015-04-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-04-15
\|\\|
\| *	Program: Do not reduce obligation types preemptively, only at	Matthieu Sozeau	2015-04-13
\| *	Fix declarations of instances to perform restriction of universe	Matthieu Sozeau	2015-04-09
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|