coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \| \|	Bump required OCaml version to 4.02.3.	Maxime Dénès	2016-12-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was decided during the working group on September, 28th.
* \| \| \| \| \| \| \| \|	Use Pp.quote in string options.	Maxime Dénès	2016-12-19
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Fix incorrect documentation that prevents successful compilation (bug #5265).	Guillaume Melquiond	2016-12-16
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Set version to 8.6 in configure.	Maxime Dénès	2016-12-08
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Windows build scripts for 8.6 final.	Maxime Dénès	2016-12-08
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Fix paths in 32-bit windows build scripts.	Maxime Dénès	2016-12-08
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Commit bumping the version number was partial...	Maxime Dénès	2016-12-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The sad part of the story is that the script testing this version number is run after tagging by the coq-dev-tools Makefile... will fix that.
\| \| \| \| \| * \| \| \|	Add bat files for 8.6rc1 build.	Maxime Dénès	2016-12-07
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Add bat files for 8.6beta1 build.	Maxime Dénès	2016-12-07
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	Set version number to 8.6rc1.	Maxime Dénès	2016-12-07
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	A few words in CHANGES.	Maxime Dénès	2016-12-07
\| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \|	ssrmatching: fix iter_constr_LR iterator wrt Proj	Enrico Tassi	2016-12-07
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-12-07
\|\ \ \ \ \ \ \ \ \ \| \| \|_\|_\|_\|/ / / / \| \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Fix #5248 - test-suite fails in 8.6beta1	Maxime Dénès	2016-12-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was yet another bug in the VM long multiplication, that I unfortunately introduced in ebc509ed2. It was impacting only 32-bit architectures. In the future, I'll try to make sure that 1) we provide unit tests for integer arithmetic (my int63 branch ships with such tests) 2) our continuous testing infrastructure runs the test suite on a 32-bit architecture. I tried to set up such an instance, but failed. Waiting for support reply.
\| * \| \| \| \| \| \| \|	Fix broken documentation in presence of \zeroone{... \tt ...}.	Guillaume Melquiond	2016-12-06
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there.
\| * \| \| \| \| \| \| \|	Update documentation (bugs #5246 and #5251).	Guillaume Melquiond	2016-12-06
\| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Merge remote-tracking branch 'github/pr/387' into v8.6	Maxime Dénès	2016-12-06
\| \|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#387: ssrmatching: handle primitive projections (fix: #5247)
\| * \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/389' into v8.6	Maxime Dénès	2016-12-06
\| \|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#389: Changed mention of deprecated -byte option to .byte suffix; change module for Coq loop
\| \| * \| \| \| \| \| \| \| \|	Change module for Coq loop	Paul Steckler	2016-12-05
\| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \|	the -byte option is deprecated	Paul Steckler	2016-12-05
\| \|/ / / / / / / / /
\| \| * \| \| \| \| \| \| \|	ssrmatching: handle primite projections (fix: #5247)	Enrico Tassi	2016-12-05
\| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \|	Compute dependency of C files only in kernel/byterun.	Maxime Dénès	2016-12-05
\| \|/ / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Some C files included in build scripts (in dev/build) were triggering errors or warnings on non-win32 platforms. Note that ide/ide_win32_stubs.c was already handled through an ad-hoc rule in Makefile. If you add a new C file outside of kernel/byterun, please extend the CFILES variable.
\| \| \| \| \| \| \| \| *	[pp] Set printing width for richpp formatter (bug #5244)	Emilio Jesus Gallego Arias	2016-12-04
\| \| \|_\|_\|_\|_\|_\|/ \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Richpp output depends on printing width, thus its internal formatter should be seeded with the proper width value. While we are at it, we increase the default buffer size to a more sensible value.
\| * \| \| \| \| \| \|	Merge remote-tracking branch 'github/pr/366' into v8.6	Maxime Dénès	2016-12-04
\| \|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#366: Univs: fix bug 5208
\| * \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/378' into v8.6	Maxime Dénès	2016-12-04
\| \|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#378: Univs: fix bug #5188
\| * \| \| \| \| \| \| \| \|	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
\| \|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#377: Univs: fix bug #5180
\| * \ \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/372' into v8.6	Maxime Dénès	2016-12-02
\| \|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes
\| * \ \ \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/368' into v8.6	Maxime Dénès	2016-12-02
\| \|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#368: Add example in dev/doc/changes involving Tacmach.project
\| * \ \ \ \ \ \ \ \ \ \ \	Merge branch 'pr/367' into v8.6	Maxime Dénès	2016-12-02
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Parts of PR#367: Fixing the "beautifier" and checking the parsing-printing reversibility
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Fixing lexing of strings in comments for beautifier.	Hugo Herbelin	2016-12-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was a bug introduced in 0ad6edc1.
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Fixing printing of "ltac:" in tactics after surrounding parentheses	Hugo Herbelin	2016-12-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	became mandatory.
\| \| \| \| \| \| * \| \| \| \| \| \| \|	Comment on universe handling in Parameters	Matthieu Sozeau	2016-12-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \|	Univs: fix bug #5188	Matthieu Sozeau	2016-12-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Parameter was implemented the wrong way trying to separate the universes of the telescope.
\| * \| \| \| \| \| \| \| \| \| \| \| \|	Merge remote-tracking branch 'github/pr/381' into v8.6	Maxime Dénès	2016-12-02
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#381: V8.6+fix typeclasses eauto shelving
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix #5242 - Dubious unsilenceable warning on invalid identifier	Maxime Dénès	2016-12-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We make this warning configurable and disabled by default.
\| \| \| * \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	with user-level notations by inserting spaces.
\| \| \| * \| \| \| \| \| \| \| \| \| \| \|	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
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#380: Fix bug #5232: proper globalization of hints paths
\| * \ \ \ \ \ \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/369' into v8.6	Maxime Dénès	2016-12-02
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#369: Make a note about wit_constr and Constrarg in dev/doc/changes
\| * \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/371' into v8.6	Maxime Dénès	2016-12-02
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#371: Update dev/doc/changes with things about mem_named_context
\| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/364' into v8.6	Maxime Dénès	2016-12-02
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#364: Add missing label. Fixes broken ref.
\| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge remote-tracking branch 'github/pr/382' into v8.6	Maxime Dénès	2016-12-02
\| \|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was PR#382: [merlin] Adjust merlin for ide.
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[merlin] Adjust merlin for ide.	Emilio Jesus Gallego Arias	2016-11-30
\| \|/ / / / / / / / / / / / / / / / /