aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
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-06Fix #5539: algebraic universe produced by cases.Gaëtan Gilbert
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-06[api] Remove dependency of library on Vernacexpr.Emilio Jesus Gallego Arias
Morally, `library` should not depend on the vernacular definition. This will also create problems when trying to modularize the codebase due to the cycle [vernacs depend for example on constrexprs]. The fix is fortunately easy.
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-05Sphinx docs: clarify strict implicit argumentsAnton Trunov
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 #5981, bugs/opened/3263.v is non-deterministic by removing the test.Théo Zimmermann
Since this is an open bug, it is of lesser importance but non-deterministic tests are a real problem OTOH.
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
2018-04-05Some advice about merge script dependencies.Théo Zimmermann
Including: how to create a GPG key.
2018-04-05Improve the MERGING doc.Théo Zimmermann
In particular, describes what to do with overlays.
2018-04-05Adapt CONTRIBUTING to recent changes in Coq.Théo Zimmermann
- The testing and benchmarking labels are now distinct. - The release manager does not take care of merging anymore. - The reference manual is not written in LaTeX anymore.
2018-04-05Merge PR #7115: Sphinx doc chapter 28Théo Zimmermann
2018-04-05Merge PR #7016: Make parsing independent of the cumulativity flag.Enrico Tassi
2018-04-05Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Enrico Tassi
2018-04-05[Sphinx] Add chapter 30Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
2018-04-05[Sphinx] Move chapter 30 to new infrastructureMaxime Dénès
2018-04-04Fixing #7100 (lost of main file location in case of Ltac failure in other file).Hugo Herbelin
2018-04-04Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Hugo Herbelin
2018-04-04check-owners.sh: add --show-patterns and --owner optionsGaëtan Gilbert
```bash $ dev/tools/check-owners.sh --show-patterns Makefile Makefile.build /Makefile*: @letouzey $ dev/tools/check-owners.sh --owner '@gares' stm/stm.ml interp/declare.ml stm/stm.ml: @gares $ dev/tools/check-owners.sh --show-patterns --owner '@gares' stm/*.ml interp/*.ml /stm/: @gares ```
2018-04-04Script to identify the code owner for given filesGaëtan Gilbert
Can be used with git diff --name-only to identify owners for changes in given commits.
2018-04-04Merge PR #7163: merge-pr.sh: cache github API callsMaxime Dénès
2018-04-04Sphinx docs: fix typo (non-ASCII character lost in sphinx migration)Peter LeFanu Lumsdaine
2018-04-04[Sphinx] Add chapter 28Maxime Dénès
Thanks to Paul Steckler for porting this chapter.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 15:04:03 +0000