aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-04-11[sphinx] Use macro |CoqIDE| consistently.Théo Zimmermann
2018-04-11Add credits related to the Sphinx migration.Théo Zimmermann
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
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
2018-04-10[Sphinx] Add chapter 6Maxime Dénès
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
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
2018-04-10[Sphinx] Add chapter 15Laurent Théry
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 look...Emilio Jesus Gallego Arias
2018-04-09Merge PR #7103: Fix #7101: STM delegation policy brokenEnrico Tassi
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
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
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 invarian...Maxime Dénès
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 (clo...Maxime Dénès
2018-04-09[Sphinx] Add chapter 7Maxime Dénès
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
2018-04-08Merge script does not warn when the remote is set to HTTPS.Théo Zimmermann
2018-04-08Merge script: use fetch URL for the remote.Théo Zimmermann
2018-04-08Merge PR #6809: Improve shell scriptsMichael Soegtrop
2018-04-08Fixes #7195 (missing freshness condition in Ltac pattern-matching names).Hugo Herbelin
2018-04-07Fixes #7192 (Print Assumptions does not enter implementation of submodules).Hugo Herbelin
2018-04-07[toplevel] Fix path initialization before vio processing (closes #7044)Emilio Jesus Gallego Arias
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 provid...Hugo Herbelin
2018-04-06Merge pull request coq/ltac2#52 from ejgallego/ltac+tacdeprPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 11:38:24 +0000