coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \| \| \| \| \| \| \|	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
\| \|/ / / / / / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	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
* \| \| \| \| \| \| \| \| \| \|	Fix locality of "Hint Resolve <->" (bug #5189).	Guillaume Melquiond	2016-11-22
\| * \| \| \| \| \| \| \| \| \|	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
\| \| \|/ / / / / \| \|/\| \| \| \| \|
\| * \| \| \| \| \|	Remove spurious spaces in merlin file generated by coq_makefile (bug #5213).	Guillaume Melquiond	2016-11-21
\| * \| \| \| \| \|	Stop parsing -compat-notations options, which are no longer supported (bug #3...	Guillaume Melquiond	2016-11-21
* \| \| \| \| \| \|	Tests for info/debug auto/eauto.	Hugo Herbelin	2016-11-19
* \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\| \| \| \| \| \|
\| * \| \| \| \| \|	Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"	Maxime Dénès	2016-11-18
\| * \| \| \| \| \|	Revert "fake_ide: use the now available Status XML message"	Maxime Dénès	2016-11-18
\| \| * \| \| \| \|	Add missing label. Fixes broken ref.	Théo Zimmermann	2016-11-17
\| \|/ / / / /
\| * \| \| \| \|	fake_ide: use the now available Status XML message	Enrico Tassi	2016-11-17