| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-08-01 | Add dev/v8-syntax/check-grammar byproducts to gitignore. | Gaëtan Gilbert | |
| 2017-08-01 | Remove obsolete files | Gaëtan Gilbert | |
| db_printers just isn't used. api.txt is superseded by the API OCaml interface. | |||
| 2017-08-01 | Add .v extension to dev/doc/notes-on-conversion | Gaëtan Gilbert | |
| This gives syntax highlighting in Coq-aware editors. | |||
| 2017-08-01 | Remove dev/TODO | Gaëtan Gilbert | |
| 2017-08-01 | Fix syntax-v8.tex bad parenthesizing | Gaëtan Gilbert | |
| Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e | |||
| 2017-08-01 | Remove unused Makefiles in dev/tools/ | Gaëtan Gilbert | |
| They seem unused since 8f4b7f1 (2007). | |||
| 2017-08-01 | Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options. | Maxime Dénès | |
| 2017-07-31 | 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-28 | 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-27 | [toplevel] Remove long ago deprecated and NOOP options. | Emilio Jesus Gallego Arias | |
| Minor clean up, no sense in having these as they do nothing. | |||
| 2017-07-27 | [api] Fix base_include LTAC parts. | Emilio Jesus Gallego Arias | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
| 2017-07-26 | Merge PR #886: Fixing what was presumably a typo in the naming conventions file | Maxime Dénès | |
| 2017-07-25 | [api] Remove type equalities from API. | Emilio Jesus Gallego Arias | |
| 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` | |||
| 2017-07-21 | Alternate way of doing timing on ci | Jason Gross | |
| This puts the boilerplate all in one place | |||
| 2017-07-21 | Separate make from python script for HoTT | Jason Gross | |
| HoTT still needs to use the submodule, but this will allow us to more easily see where the build fails, if it does | |||
| 2017-07-21 | Display timing data travis for various projects | Jason Gross | |
| 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. | |||
| 2017-07-20 | Add AppVeyor infrastructure, launching the test suite under Windows. | Maxime Dénès | |
| 2017-07-19 | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag. | Maxime Dénès | |
| 2017-07-18 | [ci] VST is now built with IGNORECOQVERSION=true. | Théo Zimmermann | |
| 2017-07-17 | [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 | |
| moved to Global). | |||
| 2017-07-17 | Merge PR #879: Adding debug printers related to universes | Maxime Dénès | |
| 2017-07-16 | Fixing what was presumably a typo in the naming conventions file. | Hugo Herbelin | |
| 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. | |||
| 2017-07-16 | Adapting to 91df40272 (body_of_constant_body moved to global). | Hugo Herbelin | |
| 2017-07-14 | 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-12 | Adding econstr printer to "include" file. | Hugo Herbelin | |
| 2017-07-11 | Merge PR #858: [travis] Remove CompCert version check hack. | Maxime Dénès | |
| 2017-07-05 | [travis] Remove CompCert version check hack. | Emilio Jesus Gallego Arias | |
| We now pass `-ignore-coq-version` to CompCert's configure (cf AbsInt/CompCert#188) , thanks to @xavierleroy . | |||
| 2017-07-05 | Makefile: fails if some .vo or .cm* file has no source | Pierre Letouzey | |
| 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 | |||
| 2017-07-04 | Revert fiat-crypto overlay | Jason Gross | |
| Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6. | |||
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-26 | 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-22 | Add missing definition and fix #use include;; as suggested by @amintimany. | Théo Zimmermann | |
| 2017-06-20 | Merge PR#774: [ide] Add route_id parameter to query call. | Maxime Dénès | |
| 2017-06-20 | Merge PR#779: Each user overlay goes into its own file. | Maxime Dénès | |
| 2017-06-18 | [ide] Add route_id parameter to query call. | Emilio Jesus Gallego Arias | |
| This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####. | |||
| 2017-06-16 | Remove -j ${NJOBS} from make invocations in the ci | Jason Gross | |
| According to https://www.gnu.org/software/make/manual/html_node/Options_002fRecursion.html#Options_002fRecursion it's not necessary, because we pass `-j ${NJOBS}` to the top-level `make` invocation in `.travis.yml`. Additionally, explicitly passing `-j` in, e.g., fiat-crypto, results in error messages such as ``` make[2]: *** write jobserver: Bad file descriptor. Stop. make[2]: *** Waiting for unfinished jobs.... make[2]: *** write jobserver: Bad file descriptor. Stop. make[1]: *** [coqprime] Error 2 make[1]: INTERNAL: Exiting with 1 jobserver tokens available; should be 2! make[1]: Leaving directory `/home/travis/build/JasonGross/coq/_build_ci/fiat-c ``` because the `-j` on the `make` in the `ci-fiat-crypto.sh` script disables jobserver mode, and the submake in fiat-crypto to make coqprime does not explicitly pass `-j`, and so reenables jobserver mode, and then `make` gets very confused. Commit made with ```bash cd dev/ci git grep --name-only -- 'make -j ${NJOBS}' | xargs sed s'/make -j \${NJOBS}/make/g' -i git grep --name-only -- 'make -f Makefile.coq -j ${NJOBS}' | xargs sed s'/make -f Makefile.coq -j \${NJOBS}/make -f Makefile.coq/g' -i ``` | |||
| 2017-06-16 | Fix ci-fiat-crypto to have a proper lite target | Jason Gross | |
| The lite target depends on having the submodule cloned to generate the list of files to not build. | |||
| 2017-06-16 | Each user overlay goes into its own file. | Théo Zimmermann | |
| This will avoid stupid merge conflicts in the future. | |||
| 2017-06-16 | Fix a bug in cumulativity | Amin Timany | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |