aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-03-14Show unused-intro-pattern warning.Théo Zimmermann
This warning was shown in CoqIDE but not by coqc.
2016-12-16Fix incorrect documentation that prevents successful compilation (bug #5265).Guillaume Melquiond
2016-12-08Set version to 8.6 in configure.Maxime Dénès
2016-12-08Windows build scripts for 8.6 final.Maxime Dénès
2016-12-08Fix paths in 32-bit windows build scripts.Maxime Dénès
2016-12-07Commit bumping the version number was partial...Maxime Dénès
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.
2016-12-07Add bat files for 8.6rc1 build.Maxime Dénès
2016-12-07Add bat files for 8.6beta1 build.Maxime Dénès
2016-12-07Set version number to 8.6rc1.Maxime Dénès
2016-12-07A few words in CHANGES.Maxime Dénès
2016-12-07ssrmatching: fix iter_constr_LR iterator wrt ProjEnrico Tassi
2016-12-06Fix #5248 - test-suite fails in 8.6beta1Maxime Dénès
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.
2016-12-06Fix broken documentation in presence of \zeroone{... \tt ...}.Guillaume Melquiond
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.
2016-12-06Update documentation (bugs #5246 and #5251).Guillaume Melquiond
2016-12-06Merge remote-tracking branch 'github/pr/387' into v8.6Maxime Dénès
Was PR#387: ssrmatching: handle primitive projections (fix: #5247)
2016-12-06Merge remote-tracking branch 'github/pr/389' into v8.6Maxime Dénès
Was PR#389: Changed mention of deprecated -byte option to .byte suffix; change module for Coq loop
2016-12-05Change module for Coq loopPaul Steckler
2016-12-05the -byte option is deprecatedPaul Steckler
2016-12-05ssrmatching: handle primite projections (fix: #5247)Enrico Tassi
2016-12-05Compute dependency of C files only in kernel/byterun.Maxime Dénès
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.
2016-12-04Merge remote-tracking branch 'github/pr/366' into v8.6Maxime Dénès
Was PR#366: Univs: fix bug 5208
2016-12-04Merge remote-tracking branch 'github/pr/378' into v8.6Maxime Dénès
Was PR#378: Univs: fix bug #5188
2016-12-02Fix test-suite after change in "context" printing.Maxime Dénès
2016-12-02Document changesMatthieu Sozeau
2016-12-02Merge remote-tracking branch 'github/pr/377' into v8.6Maxime Dénès
Was PR#377: Univs: fix bug #5180
2016-12-02Merge remote-tracking branch 'github/pr/372' into v8.6Maxime Dénès
Was PR#372: Update dev/doc/changes.txt with HintsResolveEntry changes
2016-12-02Merge remote-tracking branch 'github/pr/368' into v8.6Maxime Dénès
Was PR#368: Add example in dev/doc/changes involving Tacmach.project
2016-12-02Merge branch 'pr/367' into v8.6Maxime Dénès
Parts of PR#367: Fixing the "beautifier" and checking the parsing-printing reversibility
2016-12-02Fixing lexing of strings in comments for beautifier.Hugo Herbelin
Was a bug introduced in 0ad6edc1.
2016-12-02Fixing printing of "ltac:" in tactics after surrounding parenthesesHugo Herbelin
became mandatory.
2016-12-02Comment on universe handling in ParametersMatthieu Sozeau
2016-12-02Univs: fix bug #5188Matthieu Sozeau
Parameter was implemented the wrong way trying to separate the universes of the telescope.
2016-12-02Merge remote-tracking branch 'github/pr/381' into v8.6Maxime Dénès
Was PR#381: V8.6+fix typeclasses eauto shelving
2016-12-02Fix #5242 - Dubious unsilenceable warning on invalid identifierMaxime Dénès
We make this warning configurable and disabled by default.
2016-12-02Fixing printing of "Set Warnings Append".Hugo Herbelin
2016-12-02Fixing space in printing "Context".Hugo Herbelin
2016-12-02Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-12-02Fixing space in printing several list of implicit arguments.Hugo Herbelin
2016-12-02Fixing printing of "only parsing" in abbreviations.Hugo Herbelin
2016-12-02Protect printing of ltac's "context [...]" from possible collisionHugo Herbelin
with user-level notations by inserting spaces.
2016-12-02More on fixing #5098 (preserving printing of "in hyp").Hugo Herbelin
2016-12-02Merge remote-tracking branch 'github/pr/380' into v8.6Maxime Dénès
Was PR#380: Fix bug #5232: proper globalization of hints paths
2016-12-02Merge remote-tracking branch 'github/pr/369' into v8.6Maxime Dénès
Was PR#369: Make a note about wit_constr and Constrarg in dev/doc/changes
2016-12-02Merge remote-tracking branch 'github/pr/371' into v8.6Maxime Dénès
Was PR#371: Update dev/doc/changes with things about mem_named_context
2016-12-02Merge remote-tracking branch 'github/pr/364' into v8.6Maxime Dénès
Was PR#364: Add missing label. Fixes broken ref.
2016-12-02Merge remote-tracking branch 'github/pr/382' into v8.6Maxime Dénès
Was PR#382: [merlin] Adjust merlin for ide.
2016-11-30[merlin] Adjust merlin for ide.Emilio Jesus Gallego Arias
2016-11-30Fix shelving order in typeclasses eauto.Théo Zimmermann
Before this fix, unshelve typeclasses eauto would produce sub-goals in the reverse order compared to when they were first shelved.
2016-11-30Fix typeclasses eauto shelving.Théo Zimmermann
A file in the test-suite had to be modified. It was supposed to reproduce a behavior in intuistionistic-nuprl but it did not really. This commit is not supposed to break intuistionistic-nuprl.
2016-11-30Fix bug #5232: proper globalization of hints pathsMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 20:23:08 +0000