| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-07 | Merge PR #8868: [Docker] Update OCaml (4.07.1) and camlp5 (7.07-almost) | Emilio Jesus Gallego Arias | |
| 2018-11-07 | Merge PR #8773: [checker] Refactor by sharing code with the kernel | Pierre-Marie Pédrot | |
| 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 | [checker] Refactor by sharing code with the kernel | Maxime Dénès | |
| For historical reasons, the checker was duplicating a lot of code of the kernel. The main differences I found were bug fixes that had not been backported. With this patch, the checker uses the kernel as a library to serve the same purpose as before: validation of a `.vo` file, re-typechecking all definitions a posteriori. We also rename some files from the checker so that they don't clash with kernel files. | |||
| 2018-11-06 | Add overlay for Equations | Matthieu Sozeau | |
| 2018-11-05 | Merge PR #8515: Command driven attributes | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8843: Remove coqide ml4 | Pierre-Marie Pédrot | |
| 2018-11-03 | Merge PR #8844: Move abstract out of tactics.ml | Pierre-Marie Pédrot | |
| 2018-11-02 | Remove ml4 from Coq's make build system | Gaëtan Gilbert | |
| 2018-11-02 | Add dev/changes about attribute syntax in mlg | Gaëtan Gilbert | |
| 2018-11-02 | Add overlays (command driven attributes) | Gaëtan Gilbert | |
| 2018-11-02 | [dev doc] Update proof engine docs, fixes #6640 | Emilio Jesus Gallego Arias | |
| We update the docs for the removal of `Sigma` and the deprecation of `enter_nf`. | |||
| 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-30 | Generalizing 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-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-26 | Merge PR #8744: [dune] Compile debug and checker printers. | Gaëtan Gilbert | |
| 2018-10-26 | Merge PR #8753: [build] Refactoring of config lib and ocamldebug tweaks. | Gaëtan Gilbert | |
| 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-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.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 | [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-15 | Documenting the transition from camlp5 to coqpp for ARGUMENT EXTEND. | Pierre-Marie Pédrot | |
| 2018-10-15 | Deprecating 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-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-11 | Merge PR #186: [RFC] Coqlib cleanup | Pierre-Marie Pédrot | |
| 2018-10-11 | Merge PR #8161: Implement VERNAC EXTEND in coqpp | Maxime 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-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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |