aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2018-11-05Merge PR #8843: Remove coqide ml4Pierre-Marie Pédrot
2018-11-03Merge PR #8844: Move abstract out of tactics.mlPierre-Marie Pédrot
2018-11-02Remove ml4 from Coq's make build systemGaëtan Gilbert
2018-11-02[dev doc] Update proof engine docs, fixes #6640Emilio Jesus Gallego Arias
We update the docs for the removal of `Sigma` and the deprecation of `enter_nf`.
2018-10-31Merge PR #8688: Generalizing the various evar_map printers in Termops over ↵Pierre-Marie Pédrot
an environment
2018-10-30Merge PR #8750: [ci] [doc] Notes about branch names.Gaëtan Gilbert
2018-10-30Overlays (#8844 split-tactics)Gaëtan Gilbert
2018-10-30Adding overlay for coq-elpiHugo Herbelin
2018-10-30Generalizing the various evar_map printers in Termops over an environment.Hugo Herbelin
This is a step towards limiting calls to the global environment. Incidentally unify naming evd -> sigma in Termops.
2018-10-28Merge PR #8827: Revert "[ci] Pin CI_REF to plugin_tutorial to use not yet ↵Emilio Jesus Gallego Arias
merged commit."
2018-10-26Fix overlay for this extension of the PR. To be removed.Matthieu Sozeau
2018-10-26PR 8671: Add overlay for plugin-tutorialMatthieu Sozeau
2018-10-26Revert "[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-26Overlay for kernel entries changeMaxime Dénès
2018-10-26Merge PR #8744: [dune] Compile debug and checker printers.Gaëtan Gilbert
2018-10-26Merge PR #8753: [build] Refactoring of config lib and ocamldebug tweaks.Gaëtan Gilbert
2018-10-23[dune] [opam] Move to OPAM 2.0Emilio 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-23[dune] Compile debug and checker printers.Emilio Jesus Gallego Arias
As noted by Gäetan, we didn't compile these. We also provide a recipe to run `ocamldebug`. Try (after a build): ``` dune exec dev/dune-dbg (ocd) source dune_db ``` or ``` dune exec dev/dune-dbg checker (ocd) source checker_dune_db ``` for the checker.
2018-10-23[build] Refactoring to config lib and ocamldebug tweaks.Emilio Jesus Gallego Arias
We make `config` into a properly library. This is more uniform and useful for some clients. This also matches what was done in Dune. Next step would be to push dependencies on `Coq_config` upwards, only the actual toplevel binaries should depend on it. We also remove the stale `camlp5.dbg` and refactor the dbg files a bit, isolating the bits that are specific to the plugin / lib building method used by makefile.
2018-10-22[doc] [api] Update `odoc` to new release 1.3.0Emilio Jesus Gallego Arias
This includes many changes, please have a look at the newly generated docs.
2018-10-18Merge 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[doc] [build] Remove ocamlbuild leftovers.Emilio Jesus Gallego Arias
We had a brief leftovers of the ocamlbuild experiment that are not relevant anymore as it was removed from the tree a few years ago. p.s: The amount of cruft we have in the `dev/build/windows` folder is staggering, see for example what `git grep ocamlbuild` returns.
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-15Documenting the transition from camlp5 to coqpp for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
Those optional arguments did not really make sense. It was pretty clear from our code base, as all instances where triplicating the same type for TYPED, RAW_TYPED and GLOB_TYPED.
2018-10-15Merge 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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 18:36:04 +0000