coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\|\
* \	Efficiently generate the pretyping contexts.	Pierre-Marie Pédrot	2016-08-16
\|\ \
\| \| *	Merge branch 'pr255' into v8.5 (bug #5015)	Guillaume Melquiond	2016-08-16
\| \| \|\
\| \| \| *	Fix regression in Coqide's "forward one command" command	Xavier Leroy	2016-08-14
\| \| \|/
\| \| *	Do not assume the "TERM" environment variable is always set (bug #5007).	Guillaume Melquiond	2016-08-11
\| \| *	Use the "md5" command on OpenBSD (bug #5008).	Guillaume Melquiond	2016-08-11
* \| \|	Make code a bit clearer by removing optional argument.	Guillaume Melquiond	2016-08-10
* \| \|	Remove unused optional "predicative" argument.	Guillaume Melquiond	2016-08-10
* \| \|	Make it a bit more obvious when variables are of type unit.	Guillaume Melquiond	2016-08-10
* \| \|	Reduce warning noise when compiling the standard library.	Guillaume Melquiond	2016-08-09
* \| \|	Make List.map_filter(_i) tail-recursive.	Guillaume Melquiond	2016-08-09
\| \| *	Fix #5000: Document the native compiler soundness bug due to Unicode mangling.	Pierre-Marie Pédrot	2016-08-07
\| * \|	Using a dedicated kind of substitutions in evar name generation.	Pierre-Marie Pédrot	2016-08-06
\| * \|	Using the extended contexts in pretyping.	Pierre-Marie Pédrot	2016-08-05
\| * \|	Use sets instead of lists for names to avoid in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| * \|	Simplifying code in evar generation.	Pierre-Marie Pédrot	2016-08-04
\| * \|	Exporting the renaming API for evar declaration.	Pierre-Marie Pédrot	2016-08-04
\| * \|	Embedding the pretyping environment in a dummy record.	Pierre-Marie Pédrot	2016-08-04
\|/ /
\| *	Fix documentation typo (bug #4994).	Guillaume Melquiond	2016-08-04
\| *	Fix bug #4673: regression in setoid_rewrite.	Matthieu Sozeau	2016-07-29
* \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-29
\|\\|
\| *	Update CHANGES about #3886 bugfix	Matthieu Sozeau	2016-07-29
\| *	Fix bug #3886, generation of obligations of fixes	Matthieu Sozeau	2016-07-29
\| *	Fix #4769, univ poly and elim schemes in sections	Matthieu Sozeau	2016-07-29
* \|	COMMENT: moving misplaced comment where it belongs	Matej Kosik	2016-07-29
* \|	Adding a flag in CoqIDE to configure UNIX/Windows line ending.	Pierre-Marie Pédrot	2016-07-26
* \|	restore compatibility with gallium's camlp4 (broken by commit 8e07227c)	Pierre Letouzey	2016-07-26
\| *	Update CHANGES about critical bugfix and others	Matthieu Sozeau	2016-07-26
\| *	Merge branch 'bug4754' into v8.5	Matthieu Sozeau	2016-07-26
\| \|\
\| \| *	Fix bug #4754, allow conversion problems to remain	Matthieu Sozeau	2016-07-26
\| \|/
* \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-26
\|\\|
\| *	Merge branch 'bug4876' into v8.5	Matthieu Sozeau	2016-07-26
\| \|\
* \| \	Merge remote-tracking branch 'github/bug4679' into v8.6	Matthieu Sozeau	2016-07-25
\|\ \ \
\| \| \| *	Fix bug #4876: critical bug in guard condition checker.	Matthieu Sozeau	2016-07-25
\| \| \|/
\| * \|	Fix bug #4679, weakened setoid_rewrite unification	Matthieu Sozeau	2016-07-21
* \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-20
\|\ \ \ \| \|/ / \|/\| / \| \|/
\| *	Update CHANGES	Matthieu Sozeau	2016-07-20
\| *	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
* \|	Update CHANGES	Matthieu Sozeau	2016-07-20
* \|	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
\| *	Fix Errors.out missing a dot...	Matthieu Sozeau	2016-07-19
* \|	Complementing previous commit on fixes for printing binding patterns.	Hugo Herbelin	2016-07-19
* \|	Some extra fixes in printing patterns in binders.	Hugo Herbelin	2016-07-19
* \|	Taking into account binding patterns when agglutinating sequences of binders.	Hugo Herbelin	2016-07-19
* \|	Notations with multiple recursive binders: fixing use of alpha-conversion.	Hugo Herbelin	2016-07-19
* \|	Fixing missing parentheses in printing of patterns in binders.	Hugo Herbelin	2016-07-19
* \|	Notations: fixing multiple binders used as terms in reverse order.	Hugo Herbelin	2016-07-19
* \|	Removing a source of clash with multiple recursive patterns in notations.	Hugo Herbelin	2016-07-19
* \|	Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp).	Hugo Herbelin	2016-07-19
* \|	A new step on using alpha-conversion in printing notations.	Hugo Herbelin	2016-07-18