aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #979: Fix install-doc target and other gitlab failuresGravatar Maxime Dénès2017-09-15
|\
* \ Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Gravatar Maxime Dénès2017-09-15
|\ \ | | | | | | | | | top of the linking chain.
* \ \ Merge PR #962: Move dev/doc/changes to Markdown.Gravatar Maxime Dénès2017-09-15
|\ \ \
| | | * Fix GitLab CIGravatar Gaëtan Gilbert2017-09-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - timing needs time and python - check for compiled files without source looks in the install directory (except for make -f Makefile.ci which doesn't check), as such the install directory has been renamed to _install_ci and isn't searched.
* | | | Move README.ci and link to it from CONTRIBUTING.Gravatar Théo Zimmermann2017-09-08
| | | |
* | | | Merge PR #968: Better error messages on the CIGravatar Maxime Dénès2017-09-07
|\ \ \ \
* \ \ \ \ Merge PR #914: Making the detyper lazyGravatar Maxime Dénès2017-09-07
|\ \ \ \ \
* | | | | | Make AppVeyor generate Windows package.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Remove -debug option from Windows build script.Gravatar Maxime Dénès2017-09-05
| | | | | | | | | | | | | | | | | | | | | | | | It is no longer accepted by Coq's ./configure.
* | | | | | Get sources of cygwin packages after building the installer.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Adapt Windows build script to new CoqIDE data installation directory.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Print more of the Coq build output.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Print Coq build output.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | In regression test mode, run cygwin setup to install dependencies.Gravatar Maxime Dénès2017-09-05
| | | | | |
* | | | | | Fix Software Foundations build.Gravatar Maxime Dénès2017-09-05
| |_|_|_|/ |/| | | | | | | | | | | | | | The Software Foundations archive has been replaced by three volumes.
| * | | | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
* | | | Merge PR #999: For BZ#5688, mention hanging issue in ocamldebug and workaroundGravatar Maxime Dénès2017-08-31
|\ \ \ \
| * | | | mention issue with OCAMLRUNPARAM and ocamldebugGravatar Paul Steckler2017-08-29
| | | | |
| | | | * [general] Merge parsing with highparsing, put toplevel at the top of the ↵Gravatar Emilio Jesus Gallego Arias2017-08-29
| | |_|/ | |/| | | | | | | | | | linking chain.
* | | | 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`
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 15:21:59 +0000