coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \|	CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function	Matej Kosik	2016-08-11
* \| \| \| \| \| \|	CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function	Matej Kosik	2016-08-11
\| \| \| * \| \| \|	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
* \| \| \| \| \|	remove checker/Makefile	Pierre Letouzey	2016-07-26
* \| \| \| \| \|	No more dev/printers.cma	Pierre Letouzey	2016-07-26
* \| \| \| \| \|	Makefile.build: minor simplification	Pierre Letouzey	2016-07-26
* \| \| \| \| \|	Merge branch 'v8.6' into trunk	Pierre Letouzey	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.6'	Pierre-Marie Pédrot	2016-07-20
\|\\| \| \| \| \| \|
\| * \| \| \| \| \|	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
\| * \| \| \|	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