coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Please never mention .mli-only file in .mllib (or future .mlpack)	Pierre Letouzey	2016-06-02
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\
\| *	Fix potential race condition in vm_compute.	Guillaume Melquiond	2016-05-31
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Checker: avoid using obsolete names from Names	Pierre Letouzey	2016-05-31
\| *	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \|	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\\|
\| *	Fixing an incompatility introduced in a404360: kernel conversion was	Hugo Herbelin	2016-04-27
* \|	This is an attempt to clarify terminology in choosing variable names	Hugo Herbelin	2016-04-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\\|
* \|	Remove int64 emulation in bytecode interpreter.	Maxime Dénès	2016-03-25
\| *	A patch renaming equal into eq in the module dealing with	Hugo Herbelin	2016-03-22
\| *	Adding eq/compare/hash for syntactic view at	Hugo Herbelin	2016-03-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-18
\|\\|
\| *	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau	2016-03-10
* \|	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
\| *	Hashconsing modules.	Pierre-Marie Pédrot	2016-03-10
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\|
\| *	This fix is probably not enough to justify that there are no problems with	Maxime Dénès	2016-03-04
\| *	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \|	ADD: Names.Name.is_{anonymous,name}	Matej Kosik	2016-02-18
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-17
\|\ \
* \| \|	Term: fix a comment (first de Bruijn index is 1)	Pierre Letouzey	2016-02-16
\| * \|	Renaming variants of Entries.local_entry	Matej Kosik	2016-02-16
\| * \|	CLEANUP: Simplifying the changes done in "kernel/*"	Matej Kosik	2016-02-15
\| * \|	REFORMATTING: kernel/context.ml{,i}	Matej Kosik	2016-02-09
\| * \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ /
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\|
\| *	Fixing bde12b70 about reporting ill-formed constructor.	Hugo Herbelin	2016-01-26
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Universes algorithm : clarified comments	Jacques-Henri Jourdan	2016-01-17
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-13
\|\\|
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	COMMENTS: of "Constr.case_info" type were updated.	Matej Kosik	2016-01-11
* \| \|	COMMENTS: added to the "Names.inductive" and "Names.constructor" types.	Matej Kosik	2016-01-11
\| \| *	Be more verbose about failure to compile libraries to native code.	Guillaume Melquiond	2016-01-08
\| \| *	Fix a misleading comment for substn_vars	Matthieu Sozeau	2016-01-07
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-05
\|\\| \|
\| * \|	Fix handling of side-effects in case of `Opaque side-effects as well.	Matthieu Sozeau	2016-01-04
* \| \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
* \| \|	Avoid warnings about loop indices.	Guillaume Melquiond	2016-01-02
* \| \|	Fix typos.	Guillaume Melquiond	2016-01-01
* \| \|	Remove unused open.	Guillaume Melquiond	2016-01-01
\| * \|	Fix bug #4456, anomaly in handle-side effects	Matthieu Sozeau	2015-12-31