| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-10-04 | Merge PR #8639: [api] Be more explicit about deprecation of debug printers. | Pierre-Marie Pédrot | |
| 2018-10-04 | Test-suite: avoid explicit references to “Top” | Vincent Laporte | |
| 2018-10-04 | test-suite: cleaning | Vincent Laporte | |
| 2018-10-04 | test-suite: rename a few files | Vincent Laporte | |
| 2018-10-04 | rename test files (do not start by a digit) | Vincent Laporte | |
| 2018-10-04 | Merge PR #8322: Additional addons for Windows installer | Théo Zimmermann | |
| 2018-10-03 | Fix review change requests | Michael Soegtrop | |
| 2018-10-03 | Fix 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-03 | Merge PR #8631: [dune] Fix couple of minor bugs in #8617 | Théo Zimmermann | |
| 2018-10-03 | [build] enable warnings ok kernel/% in make based builds | Enrico 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-03 | Merge PR #8563: Fix checker soundness bug with polymorphism capturing global ↵ | Pierre-Marie Pédrot | |
| univs | |||
| 2018-10-03 | Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac ↵ | Pierre-Marie Pédrot | |
| helper. | |||
| 2018-10-03 | Rename CEphemeron.clear→clean for clarity. | whitequark | |
| 2018-10-03 | Rewrite 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-03 | Merge 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-03 | Merge PR #8456: Revert #6651: Use r.(p) syntax to print primitive projections | Hugo Herbelin | |
| 2018-10-03 | Merge PR #8629: [doc] Nits on utilities / toplevel building. | Théo Zimmermann | |
| 2018-10-03 | Merge 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-02 | Move the compat-update-process to right after branching | Jason Gross | |
| Also test that the compat updating script hasn't become outdated on the CI. | |||
| 2018-10-02 | Update the -compat flags | Jason 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-02 | Update compat notations to be compat 8.7 | Jason 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-02 | Update dev/doc/release-process: compat+automate | Jason 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 #8617 | Emilio Jesus Gallego Arias | |
| I forgot to update `.PHONY` and to put the proper flags in the new workspace file. | |||
| 2018-10-02 | Merge PR #8618: [dune] [tools] Cleanup and extra install. | Théo Zimmermann | |
| 2018-10-02 | Merge PR #8625: Fix issue #8611 - Change extensions of log files in WIndows ↵ | Théo Zimmermann | |
| build to … | |||
| 2018-10-02 | Merge PR #8623: [dune] Fix PHONY target in Dune's helper makefile. | Théo Zimmermann | |
| 2018-10-02 | Merge PR #8617: [dune] Provide workspace file with all supported Ocaml builds. | Théo Zimmermann | |
| 2018-10-02 | [ci] overlay for elpi | Enrico Tassi | |
| 2018-10-02 | Revert #6651: Use r.(p) syntax to print primitive projections | Maxime Dénès | |
| Fixes #6764: Printing Notation regressed compared to 8.7 | |||
| 2018-10-02 | Merge PR #8620: Docs: Missing backquote | Théo Zimmermann | |
| 2018-10-02 | Fix 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.0 | Emilio Jesus Gallego Arias | |
| 2018-10-02 | Merge 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-02 | Merge PR #8612: Fix issue 8610 - Change important CI DOS batch files to CRLF | Théo Zimmermann | |
| 2018-10-02 | Merge 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-02 | Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one. | Pierre-Marie Pédrot | |
| 2018-10-02 | Document the coqpp implementation of VERNAC EXTEND. | Pierre-Marie Pédrot | |
| 2018-10-02 | Port g_derive to coqpp. | Pierre-Marie Pédrot | |
| Unluckily this is the only file that contains a VERNAC EXTEND and no ARGUMENT EXTEND, which are not handled yet. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |