aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-05Merge PR #8661: CI: fix Iris and stdpp ref selectionEmilio Jesus Gallego Arias
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-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
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
2018-10-04Merge PR #8639: [api] Be more explicit about deprecation of debug printers.Pierre-Marie Pédrot
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04test-suite: rename a few filesVincent Laporte
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-10-04Merge PR #8322: Additional addons for Windows installerThéo Zimmermann
2018-10-03Fix review change requestsMichael Soegtrop
2018-10-03Fix 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[dune] Add `(package coq)` scope to artifacts.Emilio Jesus Gallego Arias
This will allow us to define extra packages such as `coq-refman`.
2018-10-03Merge PR #8631: [dune] Fix couple of minor bugs in #8617Théo Zimmermann
2018-10-03[api] Be more explicit about deprecation of debug printers.Emilio Jesus Gallego Arias
As suggested by @mattam82
2018-10-03Merge PR #8563: Fix checker soundness bug with polymorphism capturing global ↵Pierre-Marie Pédrot
univs
2018-10-03Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac ↵Pierre-Marie Pédrot
helper.
2018-10-03Rename CEphemeron.clear→clean for clarity.whitequark
2018-10-03Rewrite CEphemeron to use a type-safe implementation based on GADTs.whitequark
This eliminates 2 uses of Obj from TCB. Moreover, with the new implementation, a key that is marshalled and then unmarshalled does not compare equal with itself even using the polymorphic equality function. See the comment in CEphemeron.ml for details on implementation.
2018-10-03[pretyper] Remove imperative passing of evar_map.Emilio Jesus Gallego Arias
2018-10-03[pretyper] Less imperative passing of the evar_map, part II.Emilio Jesus Gallego Arias
This builds on the work on #8545. Some tab removal had to take place here in order to make ocp-indent work.
2018-10-03[pretyper] Less imperative passing of the evar_map, part I.Emilio Jesus Gallego Arias
This builds on the work on #8545.
2018-10-03Merge 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-03Merge PR #8456: Revert #6651: Use r.(p) syntax to print primitive projectionsHugo Herbelin
2018-10-03Merge PR #8629: [doc] Nits on utilities / toplevel building.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 03:45:13 +0000