coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\
\| *	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-24
\| \|\
\| \| *	Documenting the API of side-effects.	Pierre-Marie Pédrot	2017-03-23
\| \| *	Using a dedicated datastructure for side effect ordering.	Pierre-Marie Pédrot	2017-03-23
\| \| *	Making the side_effects type opaque.	Pierre-Marie Pédrot	2017-03-23
\| * \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\| \|\\|
\| * \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-03-22
\| \|\ \
\| * \ \	Merge PR#482: [toplevel] Remove unusable option -notop	Maxime Dénès	2017-03-22
\| \|\ \ \
\| \| \| \| *	Add a few comments in term_typing.ml.	Maxime Dénès	2017-03-21
\| \| \| \| *	Do not typecheck twice the type of opaque constants.	Maxime Dénès	2017-03-21
\| \| \| \|/
\| * \| \|	Merge PR#134: Enable `-safe-string`	Maxime Dénès	2017-03-21
\| \|\ \ \
\| \| \| \| *	In the Kami project, that causes a stack overflow in one of the example files	Paul Steckler	2017-03-20
\| \| * \| \|	[misc] Remove warnings about String.set	Emilio Jesus Gallego Arias	2017-03-20
\| \| * \| \|	[safe-string] Enable -safe-string !	Emilio Jesus Gallego Arias	2017-03-14
\| \| * \| \|	[safe_string] library/nameops	Emilio Jesus Gallego Arias	2017-03-14
\| \| * \| \|	[safe_string] kernel/cemitcodes	Emilio Jesus Gallego Arias	2017-03-14
\| \| \| * \|	[toplevel] Remove unusable option -notop	Emilio Jesus Gallego Arias	2017-03-14
\| \| * \| \|	[safe-string] kernel/nativevalues	Emilio Jesus Gallego Arias	2017-03-14
\| \| * \| \|	[safe_string] kernel/term_typing	Emilio Jesus Gallego Arias	2017-03-14
\| \| \|/ /
\| * / /	[future] Remove unused parameter greedy.	Emilio Jesus Gallego Arias	2017-03-14
\| \|/ /
\| * \|	Merge PR#189: Remove tabulation support from pretty-printing.	Maxime Dénès	2017-02-20
\| \|\ \
* \| \| \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\| \| \|
* \| \| \|	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot	2017-02-14
* \| \| \|	Reductionops now return EConstrs.	Pierre-Marie Pédrot	2017-02-14
* \| \| \|	Making judgment type generic over the type of inner constrs.	Pierre-Marie Pédrot	2017-02-14
\| * \| \|	Merge PR#393: Replace Typeops with Fast_typeops	Maxime Dénès	2017-02-08
\| \|\ \ \
\| * \ \ \	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-02-01
\| \|\ \ \ \ \| \| \| \|_\|/ \| \| \|/\| \|
\| \| * \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2017-02-01
\| \| \|\ \ \
\| \| \| \| * \|	Remove useless comments	Gaetan Gilbert	2017-01-28
\| \| \| * \| \|	[native comp] Improve error message on linking error.	Emilio Jesus Gallego Arias	2017-01-26
\| \| * \| \| \|	Do not add redundant side effects in tactic code.	Pierre-Marie Pédrot	2017-01-20
\| * \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-01-19
\| \|\\| \| \| \|
\| \| * \| \| \|	Mapping named_context_val preserves sharing when possible.	Pierre-Marie Pédrot	2017-01-17
\| \| \| * \| \|	Handle application of a primitive projection to a not yet evaluated cofixpoin...	Guillaume Melquiond	2016-12-26
\| \| * \| \| \|	Handle application of a primitive projection to a not yet evaluated cofixpoin...	Guillaume Melquiond	2016-12-23
\| * \| \| \| \|	Fixing injection in the presence of let-in in constructors.	Hugo Herbelin	2016-12-22
\| \| \| \| * \|	Replace Typeops by Fast_typeops	Gaetan Gilbert	2016-12-12
\| \| \| \| * \|	Extend Fast_typeops to be a replacement for Typeops	Gaetan Gilbert	2016-12-12
\| \| \|_\|/ / \| \|/\| \| \|
\| * \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-12-07
\| \|\\| \| \|
\| \| * \| \|	Fix #5248 - test-suite fails in 8.6beta1	Maxime Dénès	2016-12-06
\| \| * \| \|	Merge remote-tracking branch 'github/pr/366' into v8.6	Maxime Dénès	2016-12-04
\| \| \|\ \ \
\| \| \| * \| \|	Document changes	Matthieu Sozeau	2016-12-02
\| \| * \| \| \|	Merge remote-tracking branch 'github/pr/377' into v8.6	Maxime Dénès	2016-12-02
\| \| \|\ \ \ \
\| \| * \| \| \| \|	Fix #5242 - Dubious unsilenceable warning on invalid identifier	Maxime Dénès	2016-12-02
\| * \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\| \|\\| \| \| \| \|
\| \| \| * \| \| \|	Univs: fix bug #5180	Matthieu Sozeau	2016-11-30
\| \| \|/ / / /
\| \| \| * \| \|	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
\| \| \| * \| \|	Slightly more efficient [Univ.super] implem	Matthieu Sozeau	2016-11-30
\| \| \|/ / /
\| \| * \| \|	Fix incorrect long multiplication in the VM.	Guillaume Melquiond	2016-11-24