aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* [ci] [docker] Make sure we don't install optional packages with apt.Gravatar Emilio Jesus Gallego Arias2018-07-02
| | | | | | | | | | | | | This should help towards ensuring that the system only has the packages we specify in the Dockerfile. We were missing: - `git`: used in the CI system itself! - `rsync`: used in the test-suite - `python3-setuptools`, `python3-wheel`: necessary to use pip3 properly to install the missing python package. - `autoconf`, `automake`: a few CI contribs depend on them.
* Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ | | | | | | points of Camlp5
* \ Merge PR #7961: [api] Fix wrong deprecation warning (#7915)Gravatar Enrico Tassi2018-07-02
|\ \
| * | [api] Fix wrong deprecation warning (#7915)Gravatar Emilio Jesus Gallego Arias2018-07-01
|/ / | | | | | | | | | | | | Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync.
* | Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ | | | | | | | | | .git anymore.
* \ \ Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ \ | | | | | | | | | | | | Z into three files
* \ \ \ Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ \ \ | | | | | | | | | | | | | | | format).
* \ \ \ \ Merge PR #7759: Workaround to fix #7731 (printing not splitting line at ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | break hint).
* \ \ \ \ \ Merge PR #7960: [build] Remove target binary before copy.Gravatar Enrico Tassi2018-06-30
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7949: Split the Ssrmatching module between code and grammar rules.Gravatar Enrico Tassi2018-06-30
|\ \ \ \ \ \ \
| * | | | | | | Split the Ssrmatching module between code and grammar rules.Gravatar Pierre-Marie Pédrot2018-06-30
|/ / / / / / / | | | | | | | | | | | | | | | | | | | | | Fixes #7857.
| | | | | | * Adding an overlay for the PR.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | |
| | | | | | * Documenting the transition strategy of GEXTEND.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | |
| | | | | | * Port g_tactic to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | |
| | | | | | * Port g_toplevel to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | |
| | | | | | * Port g_vernac to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | |
| | | | | | * Port g_proofs to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | |
| | | | | | * Port g_constr to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | |
| | | | | | * Port g_prim to the homebrew GEXTEND parser.Gravatar Pierre-Marie Pédrot2018-06-29
| | | | | | |
| | | | | | * Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.
| | | | | * Document that GITURL variables shouldn't have a trailing .git anymore.Gravatar Théo Zimmermann2018-06-29
| |_|_|_|/ |/| | | | | | | | | | | | | | This allows to append /archive at the end.
* | | | | Merge PR #7918: Mini-update of version history with recent changes.Gravatar Théo Zimmermann2018-06-29
|\ \ \ \ \
| | | | | * Splitting primitive numeral parser/printer for positive, N, Z into three files.Gravatar Hugo Herbelin2018-06-29
| | | | | |
| | | * | | Workaround to fix #7731 (printing not splitting line at break hint).Gravatar Hugo Herbelin2018-06-29
| | | | |/ | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases, Format's inner boxes inside an outer box act as break hints, even though there are already "better" break hints in the outer box. We work around this "feature" by not inserting a box around the default printing rule for a notation if there is no effective break points in the box. See https://caml.inria.fr/mantis/view.php?id=7804 for the related OCaml discussion.
| | | | * Fixes #7712 (an anomaly in reporting bad recursive notation format).Gravatar Hugo Herbelin2018-06-29
| | | |/
* | | | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Gravatar Maxime Dénès2018-06-29
|\ \ \ \ | | | | | | | | | | | | | | | constr in Constr
| | | * | [build] Remove target binary before copy.Gravatar Emilio Jesus Gallego Arias2018-06-29
| |_|/ / |/| | | | | | | | | | | | | | | | | | | Fixes #7666. Due to shared mapping of executables Linux doesn't allow to overwrite binaries that are running; we do as `ocamlopt` and delete the target file before copy.
* | | | Merge PR #7890: Inline a function from Quote used in setoid_ring.Gravatar Maxime Dénès2018-06-29
|\ \ \ \
* \ \ \ \ Merge PR #7745: Make type Environ.globals abstract + simplify ↵Gravatar Maxime Dénès2018-06-29
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Environ.retroknowledge
* \ \ \ \ \ Merge PR #7950: Documentation for 8.8.1Gravatar Maxime Dénès2018-06-29
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
* | | | | | Merge PR #7860: Fix #7704: Launching coqide through PATH fails.Gravatar Emilio Jesus Gallego Arias2018-06-28
|\ \ \ \ \ \
| | * | | | | CHANGES for 8.8.1.Gravatar Théo Zimmermann2018-06-28
| | | | | | |
| | * | | | | Self-credit for the work done.Gravatar Théo Zimmermann2018-06-28
| |/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well.
* | | | | | Merge PR #7948: Syntax for naming an existential variableGravatar Théo Zimmermann2018-06-28
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.Gravatar Michael Soegtrop2018-06-28
|\ \ \ \ \ \ \
| | * | | | | | wrong sphinx syntaxGravatar Ambroise2018-06-28
| | | | | | | |
* | | | | | | | Merge PR #7946: Update maintainers for native/VM files in pretypingGravatar Théo Zimmermann2018-06-28
|\ \ \ \ \ \ \ \
| | | * | | | | | Update gallina-extensions.rstGravatar Ambroise2018-06-28
| |_|/ / / / / / |/| | | | | | | | | | | | | | | I knew this feature existed but I did not remember the syntax and I could not find it in the manual
* | | | | | | | Merge PR #7937: Mention Consortium in READMEGravatar Théo Zimmermann2018-06-28
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine.Gravatar Théo Zimmermann2018-06-28
|\ \ \ \ \ \ \ \ \
| | | | | | * | | | Deprecate Environ.retroknowledge function in favor of the projectionGravatar Gaëtan Gilbert2018-06-28
| | | | | | | | | |
| | | | | | * | | | [env.env_rel_context.env_rel_ctx] -> [rel_context env]Gravatar Gaëtan Gilbert2018-06-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It's a bit shorter and more direct.
| | | | | | * | | | Make Environ.globals abstract.Gravatar Gaëtan Gilbert2018-06-28
| |_|_|_|_|/ / / / |/| | | | | | | |
* | | | | | | | | Merge PR #7932: CoqIDE scrolls the proof buffer down to the first goal.Gravatar Pierre-Marie Pédrot2018-06-28
|\ \ \ \ \ \ \ \ \
| | | | * | | | | | Update maintainers for native/VM files in pretypingGravatar Maxime Dénès2018-06-28
| |_|_|/ / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7934: Add mit-plv/bedrock2-ci to CIGravatar Emilio Jesus Gallego Arias2018-06-28
|\ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | Add mit-plv/bedrock2-ci to CIGravatar Andres Erbsen2018-06-27
|/ / / / / / / / / /
* | | | | | | | | | Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Gravatar Pierre-Marie Pédrot2018-06-27
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7939: Turn the CoqProject_file module into a pure ML fileGravatar Emilio Jesus Gallego Arias2018-06-27
|\ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 07:13:25 +0000