coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing OCaml deprecated function names from the Lazy module.	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
* \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\| \|
* \| \|	Removing dead code.	Pierre-Marie Pédrot	2015-12-27
\| \| *	COMMENTS: of "Constr.case_info" type were updated.	Matej Kosik	2015-12-22
\| \| *	COMMENTS: added to the "Names.inductive" and "Names.constructor" types.	Matej Kosik	2015-12-22
\| \|/ \|/\|
\| *	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
* \|	COMMENTS: added to the "Constr.case_info" type.	Matej Kosik	2015-12-18
* \|	COMMENTS: added to some variants of the "Constr.kind_of_term" type.	Matej Kosik	2015-12-18
* \|	COMMENTS: added to the "Names" module.	Matej Kosik	2015-12-18
* \|	ALPHA-CONVERSION: in the "Reduction" module: clos_fconv --> clos_gen_conv	Matej Kosik	2015-12-17
* \|	ALPHA-CONVERSION: in the "Reduction" module: fconv --> gen_conv	Matej Kosik	2015-12-17
* \|	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
* \|	CLEANUP: in the Reduction module	Matej Kosik	2015-12-17
* \|	Fixing e3cefca41b about supposingly simplifying primitive projections	Hugo Herbelin	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-11
\|\\|
\| *	bug fixes to vm computation + test cases.	Gregory Malecha	2015-12-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-08
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-12-07
* \|	Unifying betazeta_applist and prod_applist into a clearer interface.	Hugo Herbelin	2015-12-05