Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix Software Foundations build. | 2017-09-05 | |
| | | | | The Software Foundations archive has been replaced by three volumes. | ||
* | Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaround | 2017-08-31 | |
|\ | |||
| * | mention issue with OCAMLRUNPARAM and ocamldebug | 2017-08-29 | |
| | | |||
* | | Adapt debugging doc to configure/Makefile changes. | 2017-08-29 | |
| | | |||
* | | Move debugging to Markdown. | 2017-08-29 | |
|/ | | | With a minimal diff (so I'm not putting quotes ` ` around all the code). | ||
* | Merge PR #838: Have coq-dpdgraph ci test print the differences | 2017-08-29 | |
|\ | |||
* \ | Merge PR #819: Cleanup old things | 2017-08-29 | |
|\ \ | |||
* \ \ | Merge PR #801: Make Travis generate OSX packages. | 2017-08-18 | |
|\ \ \ | |||
| * | | | Make Travis generate OSX packages. | 2017-08-17 | |
| | | | | | | | | | | | | | | | | | | | | The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq | ||
* | | | | Mention tclINDEPENDENTL (#349) in dev/doc/changes. | 2017-08-16 | |
|/ / / | |||
| * | | Add dev/v8-syntax/check-grammar byproducts to gitignore. | 2017-08-01 | |
| | | | |||
| * | | Remove obsolete files | 2017-08-01 | |
| | | | | | | | | | | | | | | | db_printers just isn't used. api.txt is superseded by the API OCaml interface. | ||
| * | | Add .v extension to dev/doc/notes-on-conversion | 2017-08-01 | |
| | | | | | | | | | | | | This gives syntax highlighting in Coq-aware editors. | ||
| * | | Remove dev/TODO | 2017-08-01 | |
| | | | |||
| * | | Fix syntax-v8.tex bad parenthesizing | 2017-08-01 | |
| | | | | | | | | | | | | Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e | ||
| * | | Remove unused Makefiles in dev/tools/ | 2017-08-01 | |
|/ / | | | | | | | They seem unused since 8f4b7f1 (2007). | ||
| * | Have coq-dpdgraph ci test print the differences | 2017-08-01 | |
|/ | | | | This allows better debugging when it fails. | ||
* | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | 2017-08-01 | |
|\ | |||
* \ | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | 2017-07-31 | |
|\ \ | |||
* \ \ | Merge PR #746: Timing on ci via coq_makefile for various projects | 2017-07-31 | |
|\ \ \ | |||
* \ \ \ | Merge PR #923: [api] Fix base_include LTAC parts. | 2017-07-28 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #782: Update API for fiat | 2017-07-28 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #852: Makefile: fails if some .vo or .cm* file has no source | 2017-07-28 | |
|\ \ \ \ \ \ | |||
| | | | | | * | [toplevel] Remove long ago deprecated and NOOP options. | 2017-07-27 | |
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | Minor clean up, no sense in having these as they do nothing. | ||
| | | * | | | [api] Fix base_include LTAC parts. | 2017-07-27 | |
| |_|/ / / |/| | | | | |||
| | | | * | deprecate Pp.std_ppcmds type alias | 2017-07-27 | |
| | | | | | |||
* | | | | | Merge PR #886: Fixing what was presumably a typo in the naming conventions file | 2017-07-26 | |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | |||
* | | | | | [api] Remove type equalities from API. | 2017-07-25 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli` | ||
| | | | * | Alternate way of doing timing on ci | 2017-07-21 | |
| | | | | | | | | | | | | | | | | | | | | This puts the boilerplate all in one place | ||
| | | | * | Separate make from python script for HoTT | 2017-07-21 | |
| | | | | | | | | | | | | | | | | | | | | HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does | ||
| | | | * | Display timing data travis for various projects | 2017-07-21 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | HoTT, which builds it's own makefile, and supports timing data, makes use of its own timing script. Everything else goes through the coq-bundled timing scripts. | ||
* | | | | | Add AppVeyor infrastructure, launching the test suite under Windows. | 2017-07-20 | |
| |_|_|/ |/| | | | |||
* | | | | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag. | 2017-07-19 | |
|\ \ \ \ | |||
* | | | | | [ci] VST is now built with IGNORECOQVERSION=true. | 2017-07-18 | |
| | | | | | |||
| * | | | | [API] Remove `open API` in ml files in favor of `-open API` flag. | 2017-07-17 | |
|/ / / / | |||
* | | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers | 2017-07-17 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵ | 2017-07-17 | |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | moved to Global). | ||
* \ \ \ \ \ | Merge PR #879: Adding debug printers related to universes | 2017-07-17 | |
|\ \ \ \ \ \ | |||
| | | | * | | | Fixing what was presumably a typo in the naming conventions file. | 2017-07-16 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed, "forall x, op x x = x" in not in the list, while this is one of the two standard meanings of idempotence. So, knowing that x, y, ... and not n are used elsewhere for variables names, and elt for constants. Moreover, it is probable that before using consistently x, y and z, I had also used m and n, sometimes. So, a convergent probability that it is (just) a typo. | ||
| | * | | | | | Adapting to 91df40272 (body_of_constant_body moved to global). | 2017-07-16 | |
| | | |/ / / | | |/| | | | |||
| * / | | | | Adding debug printers related to universes in the default debugger source file. | 2017-07-14 | |
| |/ / / / | |||
| | * | | | Fix a typo in dev/changes. | 2017-07-14 | |
| | | | | | |||
| | * | | | Document the changes in API brought by this series of patches. | 2017-07-14 | |
| |/ / / | |||
* / / / | Adding econstr printer to "include" file. | 2017-07-12 | |
|/ / / | |||
* | | | Merge PR #858: [travis] Remove CompCert version check hack. | 2017-07-11 | |
|\ \ \ | |||
| * | | | [travis] Remove CompCert version check hack. | 2017-07-05 | |
| | | | | | | | | | | | | | | | | | | | | We now pass `-ignore-coq-version` to CompCert's configure (cf AbsInt/CompCert#188) , thanks to @xavierleroy . | ||
| | * | | Makefile: fails if some .vo or .cm* file has no source | 2017-07-05 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help preventing weird compilation failures due to leftover object files after deleting or moving some source files By the way: - use plain $(filter-out ...) instead of a 'diff' macro (thanks Jason for the suggestion) - rename FIND_VCS_CLAUSE into FIND_SKIP_DIRS since it contains more than version control stuff nowadays | ||
* | | | | Revert fiat-crypto overlay | 2017-07-04 | |
|/ / / | | | | | | | | | | | | | Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6. | ||
* | | | Merge branch 'v8.6' | 2017-07-04 | |
|\ \ \ | |||
* | | | | Bump year in headers. | 2017-07-04 | |
| |/ / |/| | |