aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
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[build] enable warnings ok kernel/% in make based buildsEnrico Tassi
This is to sync with the dune build system that sets these warnings
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-03[dune] [opam] Install `revision` file when building with Dune.Emilio Jesus Gallego Arias
Fixes #8621
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
2018-10-03Merge PR #8613: [ci] [travis] Remove CI contrib testing from Travis.Gaëtan Gilbert
2018-10-02[doc] [api] Remove `ocamldoc` support in favor of `odoc`Emilio Jesus Gallego Arias
This PR removes support for `ocamldoc` in favor of `odoc`. Following a recent discussion in OCaml's discord, it turns out that basically all the ecosystem has migrated to odoc, thus we follow suit and may focus on `odoc` for Coq's ML API documentation.
2018-10-02Move the compat-update-process to right after branchingJason Gross
Also test that the compat updating script hasn't become outdated on the CI.
2018-10-02Update the -compat flagsJason Gross
Mostly via `dev/tools/update-compat.py --cur-version=8.9` We just remove test-suite/success/FunindExtraction_compat86.v because, except for the `Extraction iszero.` line at the bottom, it is a duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`). We also manually update a number of test-suite files to pre-emptively remove compatibility notations (which used to be compat 8.6, but are now compat 8.7).
2018-10-02Update compat notations to be compat 8.7Jason Gross
All changes done with ``` git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g' ``` As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and https://github.com/coq/coq/issues/8383#issuecomment-426200497
2018-10-02Update dev/doc/release-process: compat+automateJason Gross
As requested in https://github.com/coq/coq/issues/8311#issuecomment-415976318 the release process describes the steps to take. All automatable steps are taken by the new script dev/tools/update-compat.py I've tried to make the script relatively easy to update if functions get renamed or moved, but since it's doing unstructured source manipulation, it is sort-of fragile. We could plausibly add a file to the test-suite to ensure that we catch script-breakage early, but this would require dropping compatibility support much earlier in the development cycle (the compatibility changes would have to come right when the new version is branched, rather than shortly before the beta release).
2018-10-02[doc] Nits on utilities / toplevel building.Emilio Jesus Gallego Arias
2018-10-02[dune] Fix couple of minor bugs in #8617Emilio Jesus Gallego Arias
I forgot to update `.PHONY` and to put the proper flags in the new workspace file.
2018-10-02Merge PR #8618: [dune] [tools] Cleanup and extra install.Théo Zimmermann
2018-10-02Merge PR #8625: Fix issue #8611 - Change extensions of log files in WIndows ↵Théo Zimmermann
build to …
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-12 13:34:23 +0000