coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge remote-tracking branch 'github/pr/389' into v8.6	Maxime Dénès	2016-12-06
\|\
\| *	Change module for Coq loop	Paul Steckler	2016-12-05
\| *	the -byte option is deprecated	Paul Steckler	2016-12-05
\|/
*	Compute dependency of C files only in kernel/byterun.	Maxime Dénès	2016-12-05
*	Merge remote-tracking branch 'github/pr/366' into v8.6	Maxime Dénès	2016-12-04
\|\
* \	Merge remote-tracking branch 'github/pr/378' into v8.6	Maxime Dénès	2016-12-04
\|\ \
* \| \|	Fix test-suite after change in "context" printing.	Maxime Dénès	2016-12-02
\| \| *	Document changes	Matthieu Sozeau	2016-12-02
* \| \|	Merge remote-tracking branch 'github/pr/377' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \
* \ \ \	Merge remote-tracking branch 'github/pr/372' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \
* \ \ \ \	Merge remote-tracking branch 'github/pr/368' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \ \
* \ \ \ \ \	Merge branch 'pr/367' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \ \ \
\| * \| \| \| \| \|	Fixing lexing of strings in comments for beautifier.	Hugo Herbelin	2016-12-02
\| * \| \| \| \| \|	Fixing printing of "ltac:" in tactics after surrounding parentheses	Hugo Herbelin	2016-12-02
\| \| \| \| \| * \|	Comment on universe handling in Parameters	Matthieu Sozeau	2016-12-02
\| \| \| \| \| * \|	Univs: fix bug #5188	Matthieu Sozeau	2016-12-02
* \| \| \| \| \| \|	Merge remote-tracking branch 'github/pr/381' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \ \ \ \
* \| \| \| \| \| \| \|	Fix #5242 - Dubious unsilenceable warning on invalid identifier	Maxime Dénès	2016-12-02
\| \| * \| \| \| \| \|	Fixing printing of "Set Warnings Append".	Hugo Herbelin	2016-12-02
\| \| * \| \| \| \| \|	Fixing space in printing "Context".	Hugo Herbelin	2016-12-02
\| \| * \| \| \| \| \|	Fixing printers for pr_auto_using and pr_firstorder_using.	Hugo Herbelin	2016-12-02
\| \| * \| \| \| \| \|	Fixing space in printing several list of implicit arguments.	Hugo Herbelin	2016-12-02
\| \| * \| \| \| \| \|	Fixing printing of "only parsing" in abbreviations.	Hugo Herbelin	2016-12-02
\| \| * \| \| \| \| \|	Protect printing of ltac's "context [...]" from possible collision	Hugo Herbelin	2016-12-02
\| \| * \| \| \| \| \|	More on fixing #5098 (preserving printing of "in hyp").	Hugo Herbelin	2016-12-02
\| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge remote-tracking branch 'github/pr/380' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/369' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/371' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/364' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/382' into v8.6	Maxime Dénès	2016-12-02
\|\ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \|	[merlin] Adjust merlin for ide.	Emilio Jesus Gallego Arias	2016-11-30
\|/ / / / / / / / / / /
\| \| \| \| \| * \| \| \| \| \|	Fix shelving order in typeclasses eauto.	Théo Zimmermann	2016-11-30
\| \| \| \| \| * \| \| \| \| \|	Fix typeclasses eauto shelving.	Théo Zimmermann	2016-11-30
\| \|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	Fix bug #5232: proper globalization of hints paths	Matthieu Sozeau	2016-11-30
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Univs: fix bug #5180	Matthieu Sozeau	2016-11-30
\| \| \| \| \| \| \|/ /
\| \| \| \| \| \| \| *	Fix UGraph.check_eq!	Matthieu Sozeau	2016-11-30
\| \| \| \| \| \| \| *	Slightly more efficient [Univ.super] implem	Matthieu Sozeau	2016-11-30
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Fix #5183 - Two CoqIDE crash errors	Maxime Dénès	2016-11-30
* \| \| \| \| \| \|	Update copyright on documentation cover.	Maxime Dénès	2016-11-30
* \| \| \| \| \| \|	Fix #5174: Underinformative syntax error messages in the new arguments syntax	Maxime Dénès	2016-11-30
* \| \| \| \| \| \|	STM: cur_id must be invalid if an error occurs (fix #5191)	Enrico Tassi	2016-11-29
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
* \| \| \| \| \|	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
* \| \| \| \| \|	Lazily load constants in micromega (bug #5134).	Guillaume Melquiond	2016-11-24
* \| \| \| \| \|	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
* \| \| \| \| \|	Fix incorrect long multiplication in the VM.	Guillaume Melquiond	2016-11-24
* \| \| \| \| \|	Properly parenthesize "ltac:" arguments (bug #5169).	Guillaume Melquiond	2016-11-22
\| \| \| \| \| *	(v8.6) Update dev/doc/changes.txt with HintsResolveEntry changes	Jason Gross	2016-11-21
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| * \| \|	(v8.6) Update dev/doc/changes with things about mem_named_context	Jason Gross	2016-11-21
\| \|/ / / \|/\| \| \|
\| \| * \|	(v8.6) Make a note about wit_constr and Constrarg in dev/doc/changes	Jason Gross	2016-11-21
\| \|/ / \|/\| \|
\| \| *	(v8.6) Add example in dev/doc/changes involving Tacmach.project	Jason Gross	2016-11-21
\| \|/ \|/\|