aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-03Merge PR #8631: [dune] Fix couple of minor bugs in #8617Théo Zimmermann
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-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-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-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
2018-10-02Merge PR #8595: Replacing Refine.pr_constr by Termops.Internal.print_constr.Pierre-Marie Pédrot
2018-10-01Docs: Missing backquoteJoachim Breitner
2018-10-02[dune] Install more files from `tools`.Emilio Jesus Gallego Arias
These are needed for example for the test suite.
2018-10-02[tools] Remove unused / obsolete files.Emilio Jesus Gallego Arias
TTBOMK we don't use any of these files since a long time.
2018-10-01Merge PR #8531: [ci] Add plugin-tutorial to CI.Gaëtan Gilbert
2018-10-01Merge PR #8565: Make coqpp handle OCaml locationsEmilio Jesus Gallego Arias
2018-10-01Print location in OCaml code output by coqpp.Pierre-Marie Pédrot
Fixes #8018.
2018-10-01Store locations of OCaml quotations in coqpp.Pierre-Marie Pédrot
2018-10-01Merge PR #7372: Four new lemmas for listsHugo Herbelin
2018-10-01Fix issue 8610 - Change important CI DOS batch files to CRLFMichael Soegtrop
2018-10-01[ci] Add plugin-tutorial to CI.Emilio Jesus Gallego Arias
This closes #7618.
2018-10-01Merge PR #8254: Inline the definition of CClosure.mk_clos_deep.Maxime Dénès
2018-10-01Merge PR #8577: Generalize type of compare_head_with functions, and use for ↵Pierre-Marie Pédrot
econstr
2018-10-01Merge PR #8575: Remove {Safe_typing,Global}.push_contextMaxime Dénès
2018-10-01Merge PR #8579: [dune] [merlin] Fix some usability issues.Maxime Dénès
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
2018-10-01Merge PR #8177: Make the warning for non-imported hints compatible with ↵Matthieu Sozeau
internal backtracking
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:03:05 +0000