| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-09 | Adding an overlay for #8601. | Pierre-Marie Pédrot | |
| 2018-11-08 | Revert "Merge PR #8923: Bump camlp5 minimal version and use its safe API." | Pierre-Marie Pédrot | |
| This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d. | |||
| 2018-11-07 | Bump up the minimal camlp5 version to 7.06. | Pierre-Marie Pédrot | |
| This is the first release that contains the type-safe grammar API. | |||
| 2018-11-07 | Merge PR #8868: [Docker] Update OCaml (4.07.1) and camlp5 (7.07-almost) | Emilio Jesus Gallego Arias | |
| 2018-11-06 | [Docker] Update COMPILER_EDGE: 4.07.0 → 4.07.1 | Vincent Laporte | |
| Also update CAMLP5_VER_EDGE: 7.06 → 7.06.10-g84ce6cc4 This is to avoid an OCaml bug that occurs when compiling the OCaml code extracted from part of a patched version of CompCert. ~~~ File "extraction/Parser.ml", line 12375, characters 19-29: Error: Constraints are not satisfied in this type. Type initstate' should be an instance of initstate' ~~~ This compiler issue only appears with OCaml 4.07.0 (neither with 4.06 nor with 4.07.1); hence this update. | |||
| 2018-11-06 | Add overlay for Equations | Matthieu Sozeau | |
| 2018-11-05 | Merge PR #8515: Command driven attributes | Pierre-Marie Pédrot | |
| 2018-11-03 | Merge PR #8844: Move abstract out of tactics.ml | Pierre-Marie Pédrot | |
| 2018-11-02 | Add overlays (command driven attributes) | Gaëtan Gilbert | |
| 2018-10-31 | Merge PR #8688: Generalizing the various evar_map printers in Termops over ↵ | Pierre-Marie Pédrot | |
| an environment | |||
| 2018-10-30 | Merge PR #8750: [ci] [doc] Notes about branch names. | Gaëtan Gilbert | |
| 2018-10-30 | Overlays (#8844 split-tactics) | Gaëtan Gilbert | |
| 2018-10-30 | Adding overlay for coq-elpi | Hugo Herbelin | |
| 2018-10-28 | Merge PR #8827: Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet ↵ | Emilio Jesus Gallego Arias | |
| merged commit." | |||
| 2018-10-26 | Fix overlay for this extension of the PR. To be removed. | Matthieu Sozeau | |
| 2018-10-26 | PR 8671: Add overlay for plugin-tutorial | Matthieu Sozeau | |
| 2018-10-26 | Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit." | Gaëtan Gilbert | |
| This reverts commit df69c44af03f2587b3f1706a805d0e2728c1f1dc. Should be merged before any PR with plugin tutorial overlays, or we can just merge the vendor PR instead. | |||
| 2018-10-26 | Overlay for kernel entries change | Maxime Dénès | |
| 2018-10-23 | [dune] [opam] Move to OPAM 2.0 | Emilio Jesus Gallego Arias | |
| We need to update in Docker: - dune to 1.4.0: as it honors `-p` on test stanzas - dune-release to 1.1.0: support for OPAM 2.0 + fixes This makes `dune-release distrib` / `dune-release opam pkg` work. TODO: we need to figure out what is going on with the versioning. Should we do `dune subst` on `pinned`? | |||
| 2018-10-22 | [doc] [api] Update `odoc` to new release 1.3.0 | Emilio Jesus Gallego Arias | |
| This includes many changes, please have a look at the newly generated docs. | |||
| 2018-10-18 | Merge PR #8719: [ci] [appveyor] Disable validate target. | Maxime Dénès | |
| 2018-10-18 | [ci] Pin CI_REF to plugin_tutorial to use not yet merged commit. | Théo Zimmermann | |
| This fixes the CI until this commit is merged into master. | |||
| 2018-10-17 | [ci] [doc] Notes about branch names. | Emilio Jesus Gallego Arias | |
| I'd like to add this convention as it is very convenient for the development of dev tools. Example, I can do `setup-coq-devs ltac equations` and then get a fully composed tree. Similarly for preparing overlays. | |||
| 2018-10-15 | Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type. | Hugo Herbelin | |
| 2018-10-14 | [ci] [sf] Remove sed hacks from the SF build. | Emilio Jesus Gallego Arias | |
| Fixes #8337 | |||
| 2018-10-12 | [ci] [appveyor] Disable validate target. | Emilio Jesus Gallego Arias | |
| Not a big point on running the checker on Appveyor I think, this will save a bunch of time and improve reliability. | |||
| 2018-10-11 | [vernac] Remove unused abstraction from declaration_hook type. | Emilio Jesus Gallego Arias | |
| "Declaration" hooks can be polymorphic on their return type, however this facility doesn't seem used in the codebase. We thus remove the polymorphism with the hope to be able to reify the control later on. | |||
| 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 #8554: Fixes #8553: regression of tactic "change" under binders. | Pierre-Marie Pédrot | |
| 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 | [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-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 #8456: Revert #6651: Use r.(p) syntax to print primitive projections | Hugo Herbelin | |
| 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 | [ci] overlay for elpi | Enrico Tassi | |
| 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 | Merge PR #8612: Fix issue 8610 - Change important CI DOS batch files to CRLF | Théo Zimmermann | |
| 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 | |
