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