coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	COMMENT: Pre_env.env	Matej Kosik	2017-04-20
*	correcting a typo in a comment	Matej Kosik	2017-04-20
*	correcting comments in the "Context" module	Matej Kosik	2017-04-20
*	simplifying "Environ.push_named" function	Matej Kosik	2017-04-20
*	refactoring "Names.DirPath.is_empty" function	Matej Kosik	2017-04-20
*	refactoring "Names.DirPath.compare" function	Matej Kosik	2017-04-20
*	refactoring "Names.DirPath.equal" function	Matej Kosik	2017-04-20
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
* \	Merge PR#441: Port Toplevel to the Stm API	Maxime Dénès	2017-04-12
\|\ \
\| * \|	[stm] Remove edit_id.	Emilio Jesus Gallego Arias	2017-04-12
* \| \|	Merge PR#549: Fast path in weak head reduction of applied atoms.	Maxime Dénès	2017-04-11
\|\ \ \
* \ \ \	Merge PR#537: Efficient side-effect abstraction	Maxime Dénès	2017-04-11
\|\ \ \ \
\| \| * \| \|	Fast path in weak head reduction of applied atoms.	Pierre-Marie Pédrot	2017-04-08
\| \| \|/ /
* \| \| \|	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Merge PR#519: Faster side effects	Maxime Dénès	2017-04-07
\| \|\ \ \
\| \| * \| \|	Inline the only use of hcons_j in Term_typing.	Pierre-Marie Pédrot	2017-04-07
\| \| * \| \|	Documenting the fact terms are only hashconsed outside of a section.	Pierre-Marie Pédrot	2017-04-06
\| * \| \| \|	Merge PR#434: Optimizing array mapping in the kernel.	Maxime Dénès	2017-04-05
\| \|\ \ \ \
\| \| \| \| * \|	Fix substitution of abstracted lemmas.	Pierre-Marie Pédrot	2017-04-04
\| \| \|_\|/ / \| \|/\| \| \|
\| \| \| \| *	Fix bug #5435: [Eval native_compute in] raises anomaly.	Maxime Dénès	2017-04-04
* \| \| \| \|	Make the Constr.kind_of_term type parametric in sorts and universes.	Pierre-Marie Pédrot	2017-03-31
\| \| \| * \|	More efficient check in validity of side-effects.	Pierre-Marie Pédrot	2017-03-27
\| \| \| * \|	Adding the size of the opaquetab in its representation.	Pierre-Marie Pédrot	2017-03-27
\| \| \| * \|	Fix hashconsing of terms in the kernel.	Pierre-Marie Pédrot	2017-03-27
\| \| \|/ / \| \|/\| \|
* \| \| \|	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
\| \|\ \ \
\| \| \| \| *	Optimizing array mapping in the kernel.	Pierre-Marie Pédrot	2017-02-19
\| \| \| \|/
* \| \| \|	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