Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR #838: Have coq-dpdgraph ci test print the differences | Maxime Dénès | 2017-08-29 |
|\ | |||
* \ | Merge PR #819: Cleanup old things | Maxime Dénès | 2017-08-29 |
|\ \ | |||
* \ \ | Merge PR #801: Make Travis generate OSX packages. | Maxime Dénès | 2017-08-18 |
|\ \ \ | |||
| * | | | Make Travis generate OSX packages. | Maxime Dénès | 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. | Théo Zimmermann | 2017-08-16 |
|/ / / | |||
| * | | Add dev/v8-syntax/check-grammar byproducts to gitignore. | Gaëtan Gilbert | 2017-08-01 |
| | | | |||
| * | | Remove obsolete files | Gaëtan Gilbert | 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 | Gaëtan Gilbert | 2017-08-01 |
| | | | | | | | | | | | | This gives syntax highlighting in Coq-aware editors. | ||
| * | | Remove dev/TODO | Gaëtan Gilbert | 2017-08-01 |
| | | | |||
| * | | Fix syntax-v8.tex bad parenthesizing | Gaëtan Gilbert | 2017-08-01 |
| | | | | | | | | | | | | Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e | ||
| * | | Remove unused Makefiles in dev/tools/ | Gaëtan Gilbert | 2017-08-01 |
|/ / | | | | | | | They seem unused since 8f4b7f1 (2007). | ||
| * | Have coq-dpdgraph ci test print the differences | Jason Gross | 2017-08-01 |
|/ | | | | This allows better debugging when it fails. | ||
* | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | Maxime Dénès | 2017-08-01 |
|\ | |||
* \ | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | 2017-07-31 |
|\ \ | |||
* \ \ | Merge PR #746: Timing on ci via coq_makefile for various projects | Maxime Dénès | 2017-07-31 |
|\ \ \ | |||
* \ \ \ | Merge PR #923: [api] Fix base_include LTAC parts. | Maxime Dénès | 2017-07-28 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #782: Update API for fiat | Maxime Dénès | 2017-07-28 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #852: Makefile: fails if some .vo or .cm* file has no source | Maxime Dénès | 2017-07-28 |
|\ \ \ \ \ \ | |||
| | | | | | * | [toplevel] Remove long ago deprecated and NOOP options. | Emilio Jesus Gallego Arias | 2017-07-27 |
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | Minor clean up, no sense in having these as they do nothing. | ||
| | | * | | | [api] Fix base_include LTAC parts. | Emilio Jesus Gallego Arias | 2017-07-27 |
| |_|/ / / |/| | | | | |||
| | | | * | deprecate Pp.std_ppcmds type alias | Matej Košík | 2017-07-27 |
| | | | | | |||
* | | | | | Merge PR #886: Fixing what was presumably a typo in the naming conventions file | Maxime Dénès | 2017-07-26 |
|\ \ \ \ \ | |_|_|_|/ |/| | | | | |||
* | | | | | [api] Remove type equalities from API. | Emilio Jesus Gallego Arias | 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 | Jason Gross | 2017-07-21 |
| | | | | | | | | | | | | | | | | | | | | This puts the boilerplate all in one place | ||
| | | | * | Separate make from python script for HoTT | Jason Gross | 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 | Jason Gross | 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. | Maxime Dénès | 2017-07-20 |
| |_|_|/ |/| | | | |||
* | | | | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag. | Maxime Dénès | 2017-07-19 |
|\ \ \ \ | |||
* | | | | | [ci] VST is now built with IGNORECOQVERSION=true. | Théo Zimmermann | 2017-07-18 |
| | | | | | |||
| * | | | | [API] Remove `open API` in ml files in favor of `-open API` flag. | Emilio Jesus Gallego Arias | 2017-07-17 |
|/ / / / | |||
* | | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers | Maxime Dénès | 2017-07-17 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵ | Maxime Dénès | 2017-07-17 |
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | | moved to Global). | ||
* \ \ \ \ \ | Merge PR #879: Adding debug printers related to universes | Maxime Dénès | 2017-07-17 |
|\ \ \ \ \ \ | |||
| | | | * | | | Fixing what was presumably a typo in the naming conventions file. | Hugo Herbelin | 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). | Hugo Herbelin | 2017-07-16 |
| | | |/ / / | | |/| | | | |||
| * / | | | | Adding debug printers related to universes in the default debugger source file. | Pierre-Marie Pédrot | 2017-07-14 |
| |/ / / / | |||
| | * | | | Fix a typo in dev/changes. | Pierre-Marie Pédrot | 2017-07-14 |
| | | | | | |||
| | * | | | Document the changes in API brought by this series of patches. | Pierre-Marie Pédrot | 2017-07-14 |
| |/ / / | |||
* / / / | Adding econstr printer to "include" file. | Hugo Herbelin | 2017-07-12 |
|/ / / | |||
* | | | Merge PR #858: [travis] Remove CompCert version check hack. | Maxime Dénès | 2017-07-11 |
|\ \ \ | |||
| * | | | [travis] Remove CompCert version check hack. | Emilio Jesus Gallego Arias | 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 | Pierre Letouzey | 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 | Jason Gross | 2017-07-04 |
|/ / / | | | | | | | | | | | | | Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6. | ||
* | | | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-07-04 |
|\ \ \ | |||
* | | | | Bump year in headers. | Pierre-Marie Pédrot | 2017-07-04 |
| |/ / |/| | | |||
| * | | Fix libpcre dependency issue under Windows. | Maxime Dénès | 2017-06-26 |
| | | | |||
| * | | Fix proxy setting issue | Michael Soegtrop | 2017-06-26 |
| | | | |||
| * | | Fixes bug #5561,#5562 in Windows build system | Michael Soegtrop | 2017-06-26 |
| | | | |||
* | | | Add missing definition and fix #use include;; as suggested by @amintimany. | Théo Zimmermann | 2017-06-22 |
| | | | |||
* | | | Merge PR#774: [ide] Add route_id parameter to query call. | Maxime Dénès | 2017-06-20 |
|\ \ \ |