coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| *	infoH: output via msg_* to make the XML protocol happy	Enrico Tassi	2016-08-17
* \| \|	Removing dead unsafe debugging code in Constrintern.	Pierre-Marie Pédrot	2016-08-16
\| \| *	Output a break before a list only if there was an empty line (bug #4606).	Guillaume Melquiond	2016-08-16
* \| \|	Merge PR #250 into v8.6	Pierre-Marie Pédrot	2016-08-16
\|\ \ \
* \ \ \	Merge PR #237 into v8.6	Pierre-Marie Pédrot	2016-08-16
\|\ \ \ \
* \ \ \ \	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
\| \| \| * \|	Allow `STDTIME=foo make`	Jason Gross	2016-07-19
\| \|_\|/ / \|/\| \| \|
\| * \| \|	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