| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-08 | [ci] Add aac-tactics. | Théo Zimmermann | |
| And fix a typo that was previously there. | |||
| 2018-10-08 | Merge PR #8660: Issue 8659 not always build all addons | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8627: [dune] [opam] Install `revision` file when building with Dune. | Théo Zimmermann | |
| 2018-10-08 | Merge PR #8630: Some cleaning in the test suite | Enrico Tassi | |
| 2018-10-08 | Merge PR #8554: Fixes #8553: regression of tactic "change" under binders. | Pierre-Marie Pédrot | |
| 2018-10-06 | [api] Remove (most) 8.9 deprecated objects. | Emilio Jesus Gallego Arias | |
| A few of them will be of help for future cleanups. We have spared the stuff in `Names` due to bad organization of this module following the split from `Term`, which really difficult things removing the constructors. | |||
| 2018-10-06 | Merge PR #8555: Remove section paths from kernel names | Pierre-Marie Pédrot | |
| 2018-10-05 | Merge PR #8645: Improve markdown in changes. | Théo Zimmermann | |
| 2018-10-05 | Merge PR #8661: CI: fix Iris and stdpp ref selection | Emilio Jesus Gallego Arias | |
| 2018-10-05 | Fix review requests | Michael Soegtrop | |
| 2018-10-05 | Remove old folder delete (can interfere with unique folder creation) | Michael Soegtrop | |
| 2018-10-05 | Fix issue #8659 - Not always build extended set of addons for Windows installer | Michael Soegtrop | |
| 2018-10-05 | CI: fix Iris and stdpp ref selection | Gaëtan Gilbert | |
| This was broken due to a typo when introducing the archive download method. We also remove default [master] values from basic-overlay which hid this issue. | |||
| 2018-10-05 | [kernel] Remove section paths from `KerName.t` | Maxime Dénès | |
| We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code. Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not. | |||
| 2018-10-05 | Rename CHANGES to CHANGES.md. | Guillaume Melquiond | |
| 2018-10-05 | Adapt changes to backported commits. | Guillaume Melquiond | |
| 2018-10-05 | Improve markdown in changes. | Guillaume Melquiond | |
| This was mostly a matter of adding backquotes and indentation where needed. There were also some "combining grave accent" used in place of proper backquotes. I cleaned only the changes of the most recent releases. | |||
| 2018-10-05 | [ci] [dune] [opam] Fixes to OPAM and CI target. | Emilio Jesus Gallego Arias | |
| The Dune `release` profile is used by OPAM so that should cover the testing. We also update the dependencies: - camlp5: 7.01 had some bugs regarding grammar; we could use 7.02, however this version it is not in OPAM. So I guess that leaves us with 7.03 again. - lablgtk < 2.18.5 does not support OCaml >= 4.05.0. | |||
| 2018-10-04 | [CI/fiat-crypto-legacy] run cleaning script before make | Vincent Laporte | |
| 2018-10-04 | Merge PR #8636: [doc] [api] Remove `ocamldoc` support in favor of `odoc` | Théo Zimmermann | |
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
| 2018-10-03 | Fix review change requests | Michael Soegtrop | |
| 2018-10-03 | Fix issue #8321 "Add more useful addons to the Windows Installer" | Michael Soegtrop | |
| Implemented by merging addon changes in V8.8.2 (keeping everything on master) | |||
| 2018-10-03 | Merge PR #8631: [dune] Fix couple of minor bugs in #8617 | Théo Zimmermann | |
| 2018-10-03 | [dune] [opam] Install `revision` file when building with Dune. | Emilio Jesus Gallego Arias | |
| Fixes #8621 | |||
| 2018-10-03 | Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the ↵ | Théo Zimmermann | |
| compat updates to do as part of a release. | |||
| 2018-10-03 | Merge PR #8456: Revert #6651: Use r.(p) syntax to print primitive projections | Hugo Herbelin | |
| 2018-10-03 | Merge PR #8613: [ci] [travis] Remove CI contrib testing from Travis. | Gaëtan Gilbert | |
| 2018-10-02 | [doc] [api] Remove `ocamldoc` support in favor of `odoc` | Emilio Jesus Gallego Arias | |
| This PR removes support for `ocamldoc` in favor of `odoc`. Following a recent discussion in OCaml's discord, it turns out that basically all the ecosystem has migrated to odoc, thus we follow suit and may focus on `odoc` for Coq's ML API documentation. | |||
| 2018-10-02 | Move the compat-update-process to right after branching | Jason Gross | |
| Also test that the compat updating script hasn't become outdated on the CI. | |||
| 2018-10-02 | Update dev/doc/release-process: compat+automate | Jason Gross | |
| As requested in https://github.com/coq/coq/issues/8311#issuecomment-415976318 the release process describes the steps to take. All automatable steps are taken by the new script dev/tools/update-compat.py I've tried to make the script relatively easy to update if functions get renamed or moved, but since it's doing unstructured source manipulation, it is sort-of fragile. We could plausibly add a file to the test-suite to ensure that we catch script-breakage early, but this would require dropping compatibility support much earlier in the development cycle (the compatibility changes would have to come right when the new version is branched, rather than shortly before the beta release). | |||
| 2018-10-02 | [dune] Fix couple of minor bugs in #8617 | Emilio Jesus Gallego Arias | |
| I forgot to update `.PHONY` and to put the proper flags in the new workspace file. | |||
| 2018-10-02 | Merge PR #8625: Fix issue #8611 - Change extensions of log files in WIndows ↵ | Théo Zimmermann | |
| build to … | |||
| 2018-10-02 | [ci] overlay for elpi | Enrico Tassi | |
| 2018-10-02 | Fix issue #8611 - Change extensions of log files in WIndows build to ↵ | Michael Soegtrop | |
| _log.txt and _err.txt so that they can be viewed immediately in gitlab | |||
| 2018-10-02 | [ci] [travis] Remove CI contrib testing from Travis. | Emilio Jesus Gallego Arias | |
| This was kept as a fallback for some time, not worth keeping it anymore as our GitLab setup seems mature and reliable enough. | |||
| 2018-10-02 | [dune] Provide workspace file will all OCaml builds tested in CI. | Emilio Jesus Gallego Arias | |
| 2018-10-02 | Merge PR #8612: Fix issue 8610 - Change important CI DOS batch files to CRLF | Théo Zimmermann | |
| 2018-10-02 | [dune] [doc] Some tweaks to doc + per user flags. | Emilio Jesus Gallego Arias | |
| 2018-10-02 | Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0 | Pierre-Marie Pédrot | |
| 2018-10-01 | Fix issue 8610 - Change important CI DOS batch files to CRLF | Michael Soegtrop | |
| 2018-10-01 | [ci] Add plugin-tutorial to CI. | Emilio Jesus Gallego Arias | |
| This closes #7618. | |||
| 2018-10-01 | Merge PR #8579: [dune] [merlin] Fix some usability issues. | Maxime Dénès | |
| 2018-09-30 | Fix issue 8603 Move Windows CI runs to folder C:/ci | Michael Soegtrop | |
| 2018-09-30 | Typo in top_printers.ml. | Hugo Herbelin | |
| 2018-09-27 | [dune] [merlin] Fix some usability issues. | Emilio Jesus Gallego Arias | |
| As suggested on Gitter by @maximedenes we improve documentation and update Kernel's `.merlin` so it actually reports on the stricter set of warnings. We also set the language version to the proper one so users will get a better error message [the fact that we can use `(env_var ...)` with the wrong Dune version is a Dune bug indeed]. | |||
| 2018-09-27 | [ci] Allow `make ci-$contrib` when we have a build under Dune. | Emilio Jesus Gallego Arias | |
| This should allow people to test CI contribs under Dune. It should be good for now but it is still a work in progress. | |||
| 2018-09-27 | Overlays for Ltac2 and Equations. | Hugo Herbelin | |
| 2018-09-26 | [ocaml] Update required OCaml version to 4.05.0 | Emilio Jesus Gallego Arias | |
| Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml version so it makes sense we bump our dependency to 4.05.0 as we can use some newer compiler features. | |||
| 2018-09-26 | [print] Restrict use of "debug" Termops printer. | Emilio Jesus Gallego Arias | |
| The functions in `Termops.print_*` are meant to be debug printers, however, they are sometimes used in non-debug code due to a API confusion. We thus wrap such functions into an `Internal` module, improve documentation, and switch users to the right API. | |||
