aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* [Sphinx] Add chapter 6Gravatar Maxime Dénès2018-04-10
* [Sphinx] Move chapter 6 to new infrastructureGravatar Maxime Dénès2018-04-10
* Merge PR #7168: Sphinx doc chapter 15Gravatar Théo Zimmermann2018-04-10
|\
| * [Sphinx] Add chapter 15Gravatar Laurent Théry2018-04-10
| * [Sphinx] Move chapter 15 to new infrastructureGravatar Maxime Dénès2018-04-10
|/
* Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Gravatar Emilio Jesus Gallego Arias2018-04-09
|\
* \ Merge PR #7103: Fix #7101: STM delegation policy brokenGravatar Enrico Tassi2018-04-09
|\ \
* \ \ Merge PR #7207: [ci] Tentative fix for #7206: MacOS test-suite job failing.Gravatar Gaëtan Gilbert2018-04-09
|\ \ \
| * | | [ci] Tentative fix for #7206: MacOS test-suite job failing.Gravatar Théo Zimmermann2018-04-09
|/ / /
* | | Merge PR #7162: Sphinx doc chapter 7Gravatar Théo Zimmermann2018-04-09
|\ \ \
* \ \ \ Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilationGravatar Pierre-Marie Pédrot2018-04-09
|\ \ \ \
* \ \ \ \ Merge PR #7070: Clarify wording in tactics documentation.Gravatar Maxime Dénès2018-04-09
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7082: Expliciting and taking advantage of a representation invarian...Gravatar Maxime Dénès2018-04-09
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Gravatar Maxime Dénès2018-04-09
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7184: [toplevel] Fix path initialization before vio processing (clo...Gravatar Maxime Dénès2018-04-09
|\ \ \ \ \ \ \ \
| | | | | | * | | [Sphinx] Add chapter 7Gravatar Maxime Dénès2018-04-09
| | | | | | * | | [Sphinx] Make it possible to espace { by %{ in custom grammarsGravatar Maxime Dénès2018-04-09
| | | | | | * | | [Sphinx] Move chapter 7 to new infrastructureGravatar Maxime Dénès2018-04-09
| |_|_|_|_|/ / / |/| | | | | | |
* | | | | | | | Merge PR #6809: Improve shell scriptsGravatar Michael Soegtrop2018-04-08
|\ \ \ \ \ \ \ \
| | * | | | | | | [toplevel] Fix path initialization before vio processing (closes #7044)Gravatar Emilio Jesus Gallego Arias2018-04-07
| |/ / / / / / / |/| | | | | | |
* | | | | | | | Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not provid...Gravatar Hugo Herbelin2018-04-06
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6960: [api] Move some types to their proper module.Gravatar Pierre-Marie Pédrot2018-04-06
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7180: Remove unused script.Gravatar Pierre-Marie Pédrot2018-04-06
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7178: Fixes issue #7172 (don't include MinGW make in install)Gravatar Enrico Tassi2018-04-06
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | | Fix #6956: Uncaught exception in bytecode compilationGravatar Maxime Dénès2018-04-06
* | | | | | | | | | | | Merge PR #7131: Sphinx doc chapter 30Gravatar Théo Zimmermann2018-04-06
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | | | Improve shell scriptsGravatar zapashcanon2018-04-05
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #6838: Light refactoring of implicit argumentsGravatar Hugo Herbelin2018-04-05
|\ \ \ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | | | Refactor impargs code.Gravatar Jasper Hugunin2018-04-05
| | | | * | | | | | | | | Remove unused script.Gravatar Théo Zimmermann2018-04-05
| |_|_|/ / / / / / / / / |/| | | | | | | | | | |
| | | | | * | | | | | | Fix #7124: Warning "Ignoring implicit status" does not provide line numberGravatar Maxime Dénès2018-04-05
| |_|_|_|/ / / / / / / |/| | | | | | | | | |
| | | * | | | | | | | Fixes issue #7172 (don't include MinGW make in install)Gravatar Michael Soegtrop2018-04-05
* | | | | | | | | | | Merge PR #7169: Sphinx docs: fix typo in Chrząszcz (non-ASCII character lost...Gravatar Maxime Dénès2018-04-05
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7074: Update merging docGravatar Maxime Dénès2018-04-05
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
| * | | | | | | | | | | Add note for homebrew users.Gravatar Théo Zimmermann2018-04-05
| * | | | | | | | | | | Some advice about merge script dependencies.Gravatar Théo Zimmermann2018-04-05
| * | | | | | | | | | | Improve the MERGING doc.Gravatar Théo Zimmermann2018-04-05
| * | | | | | | | | | | Adapt CONTRIBUTING to recent changes in Coq.Gravatar Théo Zimmermann2018-04-05
|/ / / / / / / / / / /
* | | | | | | | | | | Merge PR #7115: Sphinx doc chapter 28Gravatar Théo Zimmermann2018-04-05
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7016: Make parsing independent of the cumulativity flag.Gravatar Enrico Tassi2018-04-05
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Gravatar Enrico Tassi2018-04-05
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | | | | [Sphinx] Add chapter 30Gravatar Maxime Dénès2018-04-05
| | | | | | * | | | | | | | [Sphinx] Move chapter 30 to new infrastructureGravatar Maxime Dénès2018-04-05
| | | | |_|/ / / / / / / / | | | |/| | | | | | | | |
* | | | | | | | | | | | | Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Gravatar Hugo Herbelin2018-04-04
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | |
* | | | | | | | | | | | | Merge PR #7163: merge-pr.sh: cache github API callsGravatar Maxime Dénès2018-04-04
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | | | | Sphinx docs: fix typo (non-ASCII character lost in sphinx migration)Gravatar Peter LeFanu Lumsdaine2018-04-04
| |_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | |
| | | | | * | | | | | | | [Sphinx] Add chapter 28Gravatar Maxime Dénès2018-04-04
| | | | | * | | | | | | | [Sphinx] Move chapter 28 to new infrastructureGravatar Maxime Dénès2018-04-04
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7158: [meta] Add `num` to the set of base libraries.Gravatar Enrico Tassi2018-04-04
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6407: Fix #6404 - Print tactics called by ML tacticsGravatar Pierre-Marie Pédrot2018-04-04
|\ \ \ \ \ \ \ \ \ \ \ \ \