aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-08Fix #5197, handling of algebraic universesMatthieu Sozeau
They were allowed to stay in terms in some cases. We now ensure that if an evar is defined as e.g. fun x => Type@{foo}, foo is properly refreshed to be non-algebraic as it could otherwise appear in the term and break the invariant. Also cleanup the implementation of refresh_universes to avoid using a mutable reference and simply rely on the Constr.map smartmap idiom instead. This might have compatibility issues, e.g. in HoTT where maybe more non-algebraic proxy universes could be generated, we'll see. For the bug report proper, there is a lack of bidirectional type-checking that makes the initial definition fail (there's a non-canonical choice of dependency if we don't consider the typing constraint). With the Program bidir hint it passes.
2018-10-08Remove dead code in universe handling in the abstract tactical.Pierre-Marie Pédrot
Since 213b323 the kernel was expecting to receive an empty set of internal universe constraints in polymorphic definitions. We lift this invariant to the code that actually generates side effects.
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 remote-tracking branch 'remotes/origin/pr/74'Pierre-Marie Pédrot
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-06Merge remote-tracking branch 'maximedenes/rm-section-path'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 #8662: Fix printing of raw terms for lambda's without parameters ↵Emilio Jesus Gallego Arias
(continued, adding smart constr_expr binder constructors)
2018-10-05[ci] Allow bedrock2 to fail.Emilio Jesus Gallego Arias
Issue #8533 is still unmitigated.
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-04Add missing indexes for Hint Cut and Hint Mode.Théo Zimmermann
2018-10-04Merge PR #8646: [dune] Add `(package coq)` scope to artifacts.Théo Zimmermann
2018-10-04Merge PR #8626: [ocaml] [lib] Remove some compatibility layers for OCaml < ↵Pierre-Marie Pédrot
4.03.0
2018-10-04Merge PR #7361: Towards selecting "best" unification failure among severalPierre-Marie Pédrot
2018-10-04Merge PR #8581: [pretyper] Remove imperative passing of evar_map.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 12:35:34 +0000