aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-10-11Merge PR #186: [RFC] Coqlib cleanupPierre-Marie Pédrot
2018-10-11Merge PR #8161: Implement VERNAC EXTEND in coqppMaxime Dénès
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2018-10-09[dune] Provide an optimized build profile with inlining reports.Emilio Jesus Gallego Arias
This satisfies a wish by @ppedrot
2018-10-08[ci] Add aac-tactics.Théo Zimmermann
And fix a typo that was previously there.
2018-10-08Merge PR #8660: Issue 8659 not always build all addonsThéo Zimmermann
2018-10-08Merge PR #8627: [dune] [opam] Install `revision` file when building with Dune.Théo Zimmermann
2018-10-08Merge PR #8630: Some cleaning in the test suiteEnrico Tassi
2018-10-08Merge 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-06Merge PR #8555: Remove section paths from kernel namesPierre-Marie Pédrot
2018-10-05Merge PR #8645: Improve markdown in changes.Théo Zimmermann
2018-10-05Merge PR #8661: CI: fix Iris and stdpp ref selectionEmilio Jesus Gallego Arias
2018-10-05Fix review requestsMichael Soegtrop
2018-10-05Remove old folder delete (can interfere with unique folder creation)Michael Soegtrop
2018-10-05Fix issue #8659 - Not always build extended set of addons for Windows installerMichael Soegtrop
2018-10-05CI: fix Iris and stdpp ref selectionGaë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-05Rename CHANGES to CHANGES.md.Guillaume Melquiond
2018-10-05Adapt changes to backported commits.Guillaume Melquiond
2018-10-05Improve 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 makeVincent Laporte
2018-10-04Merge PR #8636: [doc] [api] Remove `ocamldoc` support in favor of `odoc`Théo Zimmermann
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-10-03Fix review change requestsMichael Soegtrop
2018-10-03Fix 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-03Merge PR #8631: [dune] Fix couple of minor bugs in #8617Théo Zimmermann
2018-10-03[dune] [opam] Install `revision` file when building with Dune.Emilio Jesus Gallego Arias
Fixes #8621
2018-10-03Merge 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-03Merge PR #8456: Revert #6651: Use r.(p) syntax to print primitive projectionsHugo Herbelin
2018-10-03Merge 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-02Move the compat-update-process to right after branchingJason Gross
Also test that the compat updating script hasn't become outdated on the CI.
2018-10-02Update dev/doc/release-process: compat+automateJason 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 #8617Emilio Jesus Gallego Arias
I forgot to update `.PHONY` and to put the proper flags in the new workspace file.
2018-10-02Merge PR #8625: Fix issue #8611 - Change extensions of log files in WIndows ↵Théo Zimmermann
build to …
2018-10-02[ci] overlay for elpiEnrico Tassi
2018-10-02Fix 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-02Merge PR #8612: Fix issue 8610 - Change important CI DOS batch files to CRLFThéo Zimmermann
2018-10-02[dune] [doc] Some tweaks to doc + per user flags.Emilio Jesus Gallego Arias
2018-10-02Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.Pierre-Marie Pédrot
2018-10-02Document the coqpp implementation of VERNAC EXTEND.Pierre-Marie Pédrot
2018-10-02Pass unnamed arguments to ML macros.Pierre-Marie Pédrot
This was imposing a bit of useless burden on the API for no good reason.
2018-10-02Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0Pierre-Marie Pédrot
2018-10-01Fix issue 8610 - Change important CI DOS batch files to CRLFMichael Soegtrop
2018-10-01[ci] Add plugin-tutorial to CI.Emilio Jesus Gallego Arias
This closes #7618.
2018-10-01Merge PR #8579: [dune] [merlin] Fix some usability issues.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 18:35:18 +0000