aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2017-08-29mention issue with OCAMLRUNPARAM and ocamldebugPaul Steckler
2017-08-29[general] Merge parsing with highparsing, put toplevel at the top of the ↵Emilio Jesus Gallego Arias
linking chain.
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-29Move dev/doc/changes to Markdown.Théo Zimmermann
And remove old French part. And move part about the plugin API to the right section.
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-24Don't strip the newline, don't use \rJason Gross
Not sure entirely what it was supposed to do, but stripping the newline erased the following line
2017-08-24Swap order of "aggregating..." message and travis_foldJason Gross
Now the folded line starts with "Aggregating..." and not with "---------"
2017-08-24Only display travis_fold: on travisJason Gross
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-15Move the rest of the ci target to a bash fileJason Gross
2017-08-15Better error messages on the CIJason Gross
This makes it so that when a ci target fails, we don't get red herring error messages about .ok files not existing. Since this requires bash, we make a helper script that invokes bash, so as to not depend on bash in general.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-17 15:12:47 +0000