aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
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-08Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Hugo Herbelin
We ensure that all original names in a spine of matched nested binders are distinct. Note: This enforces that two binders with same internal names are kept disjoint but this does not enforce that we shall respect names exactly as they are printed. Only the original prefix of the internal names are preserved, not their "0" or "1" etc. suffix.
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
We fix it by looking manually for the implementation at each level of nesting rather than using the signature for the n first levels and looking for the implementation only in the n+1-th level.
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 pull request coq/ltac2#52 from ejgallego/ltac+tacdeprPierre-Marie Pédrot
[coq] Adapt to coq/coq#6960.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 12:44:58 +0000