aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-05Merge PR #8650: [ci] [dune] [opam] Fixes to OPAM and CI target.Gaëtan Gilbert
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-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-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
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 …
2018-10-02Merge PR #8623: [dune] Fix PHONY target in Dune's helper makefile.Théo Zimmermann
2018-10-02Merge PR #8617: [dune] Provide workspace file with all supported Ocaml builds.Théo Zimmermann
2018-10-02[ci] overlay for elpiEnrico Tassi
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
Fixes #6764: Printing Notation regressed compared to 8.7
2018-10-02Merge PR #8620: Docs: Missing backquoteThéo Zimmermann
2018-10-02Fix issue #8611 - Change extensions of log files in WIndows build to ↵Michael Soegtrop
_log.txt and _err.txt so that they can be viewed immediately in gitlab
2018-10-02[ci] [travis] Remove CI contrib testing from Travis.Emilio Jesus Gallego Arias
This was kept as a fallback for some time, not worth keeping it anymore as our GitLab setup seems mature and reliable enough.
2018-10-02[ocaml] [lib] Remove some compatibility layers for OCaml < 4.03.0Emilio Jesus Gallego Arias
2018-10-02Merge PR #8572: [config] Miscellaneous cleaning of configuration variables.Pierre-Marie Pédrot
2018-10-02[dune] Provide workspace file will all OCaml builds tested in CI.Emilio Jesus Gallego Arias
2018-10-02[dune] Fix PHONY target in Dune's helper makefile.Emilio Jesus Gallego Arias
2018-10-02Merge PR #8612: Fix issue 8610 - Change important CI DOS batch files to CRLFThéo Zimmermann
2018-10-02Merge PR #8614: [dune] [doc] Some tweaks to doc + per user flags.Théo Zimmermann
2018-10-02[dune] [doc] Some tweaks to doc + per user flags.Emilio Jesus Gallego Arias
2018-10-02Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0Pierre-Marie Pédrot
2018-10-02Merge PR #7823: [tactics] function to gather undef evars of the goalPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:27:07 +0000