aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2017-08-29Adapt debugging doc to configure/Makefile changes.Théo Zimmermann
2017-08-29Move debugging to Markdown.Théo Zimmermann
With a minimal diff (so I'm not putting quotes ` ` around all the code).
2017-08-29Merge PR #838: Have coq-dpdgraph ci test print the differencesMaxime Dénès
2017-08-29Merge PR #819: Cleanup old thingsMaxime Dénès
2017-08-18Merge PR #801: Make Travis generate OSX packages.Maxime Dénès
2017-08-17Make Travis generate OSX packages.Maxime Dénès
The packages will be built only for main branches (not pull requests), and are accessible via bintray: https://bintray.com/coq/coq
2017-08-16Mention tclINDEPENDENTL (#349) in dev/doc/changes.Théo Zimmermann
2017-08-01Add dev/v8-syntax/check-grammar byproducts to gitignore.Gaëtan Gilbert
2017-08-01Remove obsolete filesGaëtan Gilbert
db_printers just isn't used. api.txt is superseded by the API OCaml interface.
2017-08-01Add .v extension to dev/doc/notes-on-conversionGaëtan Gilbert
This gives syntax highlighting in Coq-aware editors.
2017-08-01Remove dev/TODOGaëtan Gilbert
2017-08-01Fix syntax-v8.tex bad parenthesizingGaëtan Gilbert
Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e
2017-08-01Remove unused Makefiles in dev/tools/Gaëtan Gilbert
They seem unused since 8f4b7f1 (2007).
2017-08-01Have coq-dpdgraph ci test print the differencesJason Gross
This allows better debugging when it fails.
2017-08-01Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Maxime Dénès
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-31Merge PR #746: Timing on ci via coq_makefile for various projectsMaxime Dénès
2017-07-28Merge PR #923: [api] Fix base_include LTAC parts.Maxime Dénès
2017-07-28Merge PR #782: Update API for fiatMaxime Dénès
2017-07-28Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceMaxime 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-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Merge PR #886: Fixing what was presumably a typo in the naming conventions fileMaxime 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-21Alternate way of doing timing on ciJason Gross
This puts the boilerplate all in one place
2017-07-21Separate make from python script for HoTTJason 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-21Display timing data travis for various projectsJason 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-20Add AppVeyor infrastructure, launching the test suite under Windows.Maxime Dénès
2017-07-19Merge 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-17Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersMaxime Dénès
2017-07-17Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵Maxime Dénès
moved to Global).
2017-07-17Merge PR #879: Adding debug printers related to universesMaxime Dénès
2017-07-16Fixing 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-16Adapting to 91df40272 (body_of_constant_body moved to global).Hugo Herbelin
2017-07-14Adding debug printers related to universes in the default debugger source file.Pierre-Marie Pédrot
2017-07-14Fix a typo in dev/changes.Pierre-Marie Pédrot
2017-07-14Document the changes in API brought by this series of patches.Pierre-Marie Pédrot
2017-07-12Adding econstr printer to "include" file.Hugo Herbelin
2017-07-11Merge 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-05Makefile: fails if some .vo or .cm* file has no sourcePierre 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-04Revert fiat-crypto overlayJason Gross
Not a useful overlay. Fiat-crypto has since been updated to pass -compat 8.6.
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-26Fix libpcre dependency issue under Windows.Maxime Dénès
2017-06-26Fix proxy setting issueMichael Soegtrop
2017-06-26Fixes bug #5561,#5562 in Windows build systemMichael Soegtrop
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:30:25 +0000