| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | 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-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 | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |