aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-09Simplify code for [Definition := Eval ...]Gaëtan Gilbert
Note that since this now reduces before restricting universes behaviour may be a bit different.
2018-10-09Fix nativenorm when an evar is in the wrong place.Gaëtan Gilbert
See commit [Simplify code for [Definition := Eval ...]] which without this breaks test suite 7631.v
2018-10-09Merge PR #8632: [ide] [dune] [test-suite] Reorganize `fake_ide` build.Pierre-Marie Pédrot
2018-10-08Merge PR #8676: Fixes #8672: ill-formed pattern substitution in notation ↵Emilio Jesus Gallego Arias
with "let"
2018-10-08Merge PR #8674: [ci] Add aac-tactics.Emilio Jesus Gallego Arias
2018-10-08Fixes #8672 (ill-formed pattern substitution in notation with "let").Hugo Herbelin
2018-10-08[ide] [dune] [test-suite] Reorganize `fake_ide` build.Emilio Jesus Gallego Arias
Even if `fake_ide` was under tools, it depended on libraries from `ide`. Thus, we move `fake_ide` to `ide`, and make it "private" to the test-suite [this means `test-suite` depends on the `ide` folder then]. In the Dune side, we reorganize libraries so `fake_ide` doesn't depend on GTK anymore, this allows to run the test-suite when GTK is not available. In order to achieve this, we had to split the `coqide` package in a server and client version.
2018-10-08[ci] Add aac-tactics.Théo Zimmermann
And fix a typo that was previously there.
2018-10-08Merge PR #8677: [dune] Fix bad interaction among PR #8627 and #8657Maxime Dénès
2018-10-08[dune] Fix bad interaction among PR #8627 and #8657Emilio Jesus Gallego Arias
Dangers of not stacking PRs hit again, and here we hit a problem breaking the build on master due to #8627 adding a new file to install with for the (implicit) `coq` package and #8657 removing the implicit status of such package.
2018-10-08Merge PR #8657: [dune] Refactor files following advice from upstream.Théo Zimmermann
2018-10-08Merge PR #8654: Remove FCast from CClosure.fterm.Maxime Dénès
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 #8585: Simplify declaration of universe namesPierre-Marie Pédrot
2018-10-08Merge PR #8668: Missing headers in two filesThé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-08Merge PR #8582: [api] Deprecate `evar_map` ref combinators.Pierre-Marie Pédrot
2018-10-07Adding missing header in functional_principles_types.ml.Hugo Herbelin
2018-10-07Adding missing header to comFixpoint.ml.Hugo Herbelin
2018-10-07[api] Deprecate `evar_map` ref combinators.Emilio Jesus Gallego Arias
All the `evar_map` APIs were deprecated in 8.9, thus we deprecate the combinators to discourage this style of programming. Still a few places do use imperative style, but they are pretty localized and should be cleaned up separately. As these are the last bits of `e_` API remaining this PR closes #6342.
2018-10-07Merge PR #8493: [api] Remove (most) 8.9 deprecated objects.Pierre-Marie Pédrot
2018-10-06Merge PR #7850: Rewrite CEphemeron to use a type-safe implementation based ↵Pierre-Marie Pédrot
on GADTs
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 #8662: Fix printing of raw terms for lambda's without parameters ↵Emilio Jesus Gallego Arias
(continued, adding smart constr_expr binder constructors)
2018-10-05Merge PR #8658: Remove duplicate committers.Théo Zimmermann
2018-10-05Merge PR #8645: Improve markdown in changes.Théo Zimmermann
2018-10-05[dune] Refactor files following advice from upstream.Emilio Jesus Gallego Arias
After some discussion upstream, I think that for the current a multi-package setup in a single repository this setup saves a bit work. The most problematic bit is the `-rectypes` flag; its status is not saved per-library so we must either duplicate the flags in the coqide scope (scope == dune-project file), or unify its scope with Coq. We do this last option as this seems like the easiest thing for now. Changes: - Move coqide.opam file to the root, use a single scope/`dune-project` file. - Remove `dune-workspace`, this should be owned by the developer / user.
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-05Merge PR #8650: [ci] [dune] [opam] Fixes to OPAM and CI target.Gaëtan Gilbert
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-05Using smart mkLambdaCN/mkProdCN.Hugo Herbelin
2018-10-05Documenting constr_expr constructors; adding smart CLam/CProd.Hugo Herbelin
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-05Remove duplicate committers.Guillaume Melquiond
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-05Merge PR #8653: [CI/fiat-crypto-legacy] run cleaning script before makeEmilio Jesus Gallego Arias
2018-10-04Remove FCast from CClosure.fterm.Pierre-Marie Pédrot
Just like in the Sixth Sense, it turns out it was dead code all along.
2018-10-04Simplify declaration of universe namesGaëtan Gilbert
Declaring the universe to the kernel/section mechanism is centralized to [Declare.declare_universe_context]. Then the universe name object really is only about the user visible names.
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-04Merge PR #8646: [dune] Add `(package coq)` scope to artifacts.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 08:06:56 +0000