aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
...
* | | | Adapt debugging doc to configure/Makefile changes.Gravatar Théo Zimmermann2017-08-29
| | | |
* | | | Move debugging to Markdown.Gravatar Théo Zimmermann2017-08-29
|/ / / | | | | | | With a minimal diff (so I'm not putting quotes ` ` around all the code).
| | * Move dev/doc/changes to Markdown.Gravatar Théo Zimmermann2017-08-29
| |/ |/| | | | | | | And remove old French part. And move part about the plugin API to the right section.
* | Merge PR #838: Have coq-dpdgraph ci test print the differencesGravatar Maxime Dénès2017-08-29
|\ \
* \ \ Merge PR #819: Cleanup old thingsGravatar Maxime Dénès2017-08-29
|\ \ \
| | | * Don't strip the newline, don't use \rGravatar Jason Gross2017-08-24
| | | | | | | | | | | | | | | | | | | | Not sure entirely what it was supposed to do, but stripping the newline erased the following line
| | | * Swap order of "aggregating..." message and travis_foldGravatar Jason Gross2017-08-24
| | | | | | | | | | | | | | | | | | | | Now the folded line starts with "Aggregating..." and not with "---------"
| | | * Only display travis_fold: on travisGravatar Jason Gross2017-08-24
| | | |
* | | | Merge PR #801: Make Travis generate OSX packages.Gravatar Maxime Dénès2017-08-18
|\ \ \ \
| * | | | Make Travis generate OSX packages.Gravatar Maxime Dénès2017-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.Gravatar Théo Zimmermann2017-08-16
|/ / / /
| | | * Move the rest of the ci target to a bash fileGravatar Jason Gross2017-08-15
| | | |
| | | * Better error messages on the CIGravatar Jason Gross2017-08-15
| |_|/ |/| | | | | | | | | | | | | | | | | | | | 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.
| * | Add dev/v8-syntax/check-grammar byproducts to gitignore.Gravatar Gaëtan Gilbert2017-08-01
| | |
| * | Remove obsolete filesGravatar Gaëtan Gilbert2017-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-conversionGravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | This gives syntax highlighting in Coq-aware editors.
| * | Remove dev/TODOGravatar Gaëtan Gilbert2017-08-01
| | |
| * | Fix syntax-v8.tex bad parenthesizingGravatar Gaëtan Gilbert2017-08-01
| | | | | | | | | | | | Introduced c1e9a27d383688e44ba34ada24fe08151cb5846e
| * | Remove unused Makefiles in dev/tools/Gravatar Gaëtan Gilbert2017-08-01
|/ / | | | | | | They seem unused since 8f4b7f1 (2007).
| * Have coq-dpdgraph ci test print the differencesGravatar Jason Gross2017-08-01
|/ | | | This allows better debugging when it fails.
* Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.Gravatar Maxime Dénès2017-08-01
|\
* \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
* \ \ Merge PR #746: Timing on ci via coq_makefile for various projectsGravatar Maxime Dénès2017-07-31
|\ \ \
* \ \ \ Merge PR #923: [api] Fix base_include LTAC parts.Gravatar Maxime Dénès2017-07-28
|\ \ \ \
* \ \ \ \ Merge PR #782: Update API for fiatGravatar Maxime Dénès2017-07-28
|\ \ \ \ \
* \ \ \ \ \ Merge PR #852: Makefile: fails if some .vo or .cm* file has no sourceGravatar Maxime Dénès2017-07-28
|\ \ \ \ \ \
| | | | | | * [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | Minor clean up, no sense in having these as they do nothing.
| | | * | | [api] Fix base_include LTAC parts.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |_|/ / / |/| | | |
| | | | * deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | | |
* | | | | Merge PR #886: Fixing what was presumably a typo in the naming conventions fileGravatar Maxime Dénès2017-07-26
|\ \ \ \ \ | |_|_|_|/ |/| | | |
* | | | | [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-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 ciGravatar Jason Gross2017-07-21
| | | | | | | | | | | | | | | | | | | | This puts the boilerplate all in one place
| | | | * Separate make from python script for HoTTGravatar Jason Gross2017-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 projectsGravatar Jason Gross2017-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.Gravatar Maxime Dénès2017-07-20
| |_|_|/ |/| | |
* | | | Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Maxime Dénès2017-07-19
|\ \ \ \
* | | | | [ci] VST is now built with IGNORECOQVERSION=true.Gravatar Théo Zimmermann2017-07-18
| | | | |
| * | | | [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
|/ / / /
* | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersGravatar Maxime Dénès2017-07-17
|\ \ \ \
* \ \ \ \ Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body ↵Gravatar Maxime Dénès2017-07-17
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | moved to Global).
* \ \ \ \ \ Merge PR #879: Adding debug printers related to universesGravatar Maxime Dénès2017-07-17
|\ \ \ \ \ \
| | | | * | | Fixing what was presumably a typo in the naming conventions file.Gravatar Hugo Herbelin2017-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).Gravatar Hugo Herbelin2017-07-16
| | | |/ / / | | |/| | |
| * / | | | Adding debug printers related to universes in the default debugger source file.Gravatar Pierre-Marie Pédrot2017-07-14
| |/ / / /
| | * | | Fix a typo in dev/changes.Gravatar Pierre-Marie Pédrot2017-07-14
| | | | |
| | * | | Document the changes in API brought by this series of patches.Gravatar Pierre-Marie Pédrot2017-07-14
| |/ / /
* / / / Adding econstr printer to "include" file.Gravatar Hugo Herbelin2017-07-12
|/ / /
* | | Merge PR #858: [travis] Remove CompCert version check hack.Gravatar Maxime Dénès2017-07-11
|\ \ \
| * | | [travis] Remove CompCert version check hack.Gravatar Emilio Jesus Gallego Arias2017-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 sourceGravatar Pierre Letouzey2017-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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 02:56:59 +0000