aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-04-12Merge PR #7202: Correction of ugly message described in #4667Pierre Courtieu
2018-04-12Merge PR #7220: Many Sphinx fixes (including a fix of the credits chapter)Maxime Dénès
2018-04-12Merge PR #7201: Translation fixes in chapter syntax extensions.Maxime Dénès
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-04-12Merge PR #500: Move bugs that have been closed on BugzillaMaxime Dénès
2018-04-12Fixing the 3 cases of a "Stream.Error" ended with two periods.Hugo Herbelin
The "Stream.Error" printer does add a period, so, the messages themselves should not.
2018-04-12Merge PR #7087: Congruence tactic engine updatePierre-Marie Pédrot
2018-04-12Merge PR #7096: coqide: avoid marking sentences that are not in the document ↵Pierre-Marie Pédrot
anymore
2018-04-12Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac ↵Pierre-Marie Pédrot
failure in other file
2018-04-12[Sphinx] Add chapter 29Maxime Dénès
Thanks to Clément Pit Claudel for porting this chapter. Backport universe polymorphism changes from 2017 and 2018.
2018-04-12Attempt to fix the doubly encapsulated Ltac errors in coqide.Hugo Herbelin
It seems that ExplainErr.process_vernac_interp_error is called twice in CoqIDE. First time in Stm.stm_vernac_interp (via Stm.call_process_error_once). Second time in the "handle_exn" method used by CoqIDE to handle exceptions coming from Coq (ide_slave.ml/xmlprotocol.ml). The proposed fix is to remove the call in CoqIDE, assuming that the process_vernac_interp_error call is done otherwise on all potential error paths.
2018-04-11[sphinx] Remove migration artefacts.Théo Zimmermann
These were used very inconsistenty, serve no purpose and the link to the source is particularly useless because it's a moving target.
2018-04-11[Sphinx] Move chapter 29 to new infrastructureMaxime Dénès
2018-04-11Fix the status of some resolved bugsTej Chajed
2018-04-11[sphinx] Use macros for notes and examples.Théo Zimmermann
2018-04-11[sphinx] Fixes in chapter 2.Théo Zimmermann
Mostly using the good option macros.
2018-04-11Remove empty reference to the current version of Coq.Théo Zimmermann
2018-04-11[sphinx] Use macro |CoqIDE| consistently.Théo Zimmermann
2018-04-11Add credits related to the Sphinx migration.Théo Zimmermann
Closes #7209.
2018-04-11merge script support https + typos in docPierre Courtieu
2018-04-11Correction of ugly message described in #4667Julien Forest
2018-04-11Fix wrong mention in the release notes.Théo Zimmermann
2018-04-11Merge PR #7102: Improvements to the merge script.Maxime Dénès
2018-04-11Merge PR #7203: removing ugly error message of #5147Pierre Courtieu
2018-04-11Merge PR #7218: Add myself as the primary maintainer of the warnings systemEmilio Jesus Gallego Arias
2018-04-11[warnings] Remove `set_current_loc` hack.Emilio Jesus Gallego Arias
Instead of the current hack that won't work as soon as we check some part of the document asynchronously, we make the warning processor recover a proper location if the warning doesn't have one attached. This is what CoqIDE does [but it queries it's own document model]. Fixes: #6172
2018-04-11Add myself as the primary maintainer of the warnings systemMaxime Dénès
2018-04-11Merge PR #6955: Fixed many typos and grammar errors in chapter 11 of the manual.Maxime Dénès
2018-04-11Adding an overlay for Ltac2.Pierre-Marie Pédrot
2018-04-11Fix compilation w.r.t. coq/coq#7213.Pierre-Marie Pédrot
2018-04-10Merge PR #7020: Sphinx doc chapter 6Théo Zimmermann
2018-04-10Deprecate the "simple subst" tactic.Pierre-Marie Pédrot
This tactic was introduced by aba4b19 in 2009 and never documented. Its main purpose was backward compatibility, and as such it ought to be deprecated.
2018-04-10[Sphinx] Add chapter 6Maxime Dénès
Thanks to Yves Bertot for porting this chapter.
2018-04-10[Sphinx] Move chapter 6 to new infrastructureMaxime Dénès
2018-04-10Replace uses of Termops.dependent by more specific functions.Pierre-Marie Pédrot
This is more efficient in general, because Termops.dependent doesn't take advantage of the knowledge of its pattern argument.
2018-04-10Merge PR #7168: Sphinx doc chapter 15Théo Zimmermann
2018-04-10Do not compute constr matching context if not used.Pierre-Marie Pédrot
This mitigates bug #6860.
2018-04-10[Sphinx] Add chapter 15Laurent Théry
Thanks to Laurent Théry for porting this chapter.
2018-04-10[Sphinx] Move chapter 15 to new infrastructureMaxime Dénès
2018-04-09change error message in #5147Julien Forest
2018-04-09Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while ↵Emilio Jesus Gallego Arias
looking for a notation for a nested pattern
2018-04-09Merge PR #7103: Fix #7101: STM delegation policy brokenEnrico Tassi
# Conflicts: # CHANGES
2018-04-09Merge PR #7207: [ci] Tentative fix for #7206: MacOS test-suite job failing.Gaëtan Gilbert
2018-04-09[ci] Tentative fix for #7206: MacOS test-suite job failing.Théo Zimmermann
2018-04-09Merge PR #7162: Sphinx doc chapter 7Théo Zimmermann
2018-04-09Merge script: adds a way for confirmation to expect a newline.Théo Zimmermann
This fulfils Gaetan's wish.
2018-04-09removing uggly error message of #5147Julien Forest
2018-04-09Translation fixes in chapter syntax extensions.Hugo Herbelin
2018-04-09Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationPierre-Marie Pédrot
2018-04-09Add sanity check in merge script: local branch is up-to-date.Théo Zimmermann
In case the local branch is ahead of upstream, we only print a warning because it could be that we are merging several PRs in a row.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 06:54:12 +0000