aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-10Merge PR #7020: Sphinx doc chapter 6Théo Zimmermann
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-10Merge PR #7168: Sphinx doc chapter 15Théo Zimmermann
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-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.
2018-04-09Merge PR #7070: Clarify wording in tactics documentation.Maxime Dénès
2018-04-09Merge PR #7082: Expliciting and taking advantage of a representation ↵Maxime Dénès
invariant in Esubst
2018-04-09Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Maxime Dénès
2018-04-09Merge PR #7184: [toplevel] Fix path initialization before vio processing ↵Maxime Dénès
(closes #7044)
2018-04-09[Sphinx] Add chapter 7Maxime Dénès
Thanks to Laurent Théry for porting this chapter.
2018-04-09[Sphinx] Make it possible to espace { by %{ in custom grammarsMaxime Dénès
2018-04-09[Sphinx] Move chapter 7 to new infrastructureMaxime Dénès
2018-04-08Document requirement to have git >= 2.7 to use the merge script.Théo Zimmermann
As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
2018-04-08Merge script does not warn when the remote is set to HTTPS.Théo Zimmermann
This should solve Emilio's problem.
2018-04-08Merge script: use fetch URL for the remote.Théo Zimmermann
In case the push URL has been overriden to make it fetch-only.
2018-04-08Merge PR #6809: Improve shell scriptsMichael Soegtrop
2018-04-07[toplevel] Fix path initialization before vio processing (closes #7044)Emilio Jesus Gallego Arias
The toplevel refactoring made path initialization per document, however vio-checking and vio-tasks are not documents, so loadpath must be initialized individually. Patch by @gares, refactoring to avoid double-initialization by me. Co-authored-by: <Enrico.Tassi@inria.fr>
2018-04-06Fixed many typos and grammar errors in chapter 11 of the manual.Zeimer
2018-04-06Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not ↵Hugo Herbelin
provide line number
2018-04-06Merge PR #6960: [api] Move some types to their proper module.Pierre-Marie Pédrot
2018-04-06Merge PR #7180: Remove unused script.Pierre-Marie Pédrot
2018-04-06Merge PR #7178: Fixes issue #7172 (don't include MinGW make in install)Enrico Tassi
2018-04-06Fix #6956: Uncaught exception in bytecode compilationMaxime Dénès
We also make the code of [compact] in kernel/univ.ml a bit clearer.
2018-04-06Merge PR #7131: Sphinx doc chapter 30Théo Zimmermann
2018-04-05Improve shell scriptszapashcanon
2018-04-05Merge PR #6838: Light refactoring of implicit argumentsHugo Herbelin
2018-04-05Refactor impargs code.Jasper Hugunin
This should preserve semantics exactly. In the compute_implicits family of functions, I changed the name of the pushed rel to not be fresh, but the env isn't passed to find_displayed_name_in, and shouldn't affect whd_all.
2018-04-05Remove unused script.Théo Zimmermann
This is dead code since fd44a40f9d426a7b65f167bc30d320a0f7dd2bbd. This script was initially introduced in a088d03434417e935df3c75f81a954eadbdfc2b8 and left untouched since then.
2018-04-05Fix #7124: Warning "Ignoring implicit status" does not provide line numberMaxime Dénès
2018-04-05Fixes issue #7172 (don't include MinGW make in install)Michael Soegtrop
2018-04-05Merge PR #7169: Sphinx docs: fix typo in Chrząszcz (non-ASCII character ↵Maxime Dénès
lost in sphinx migration)
2018-04-05Merge PR #7074: Update merging docMaxime Dénès
2018-04-05Add note for homebrew users.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 07:12:52 +0000