aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-09[travis] Add explicit opam switch command to guarantee we're using the ↵Théo Zimmermann
requested compiler.
2018-05-09[travis] Fix version of camlp5 for OCaml 4.06.1.Théo Zimmermann
2018-05-09use at least 6 Xs in mktemp filename templatesSven M. Hallberg
OpenBSD mktemp fails with an error otherwise.
2018-05-09test for coqc -oEnrico Tassi
2018-05-09checkpointYves Bertot
2018-05-09trying to force the resolution of type classes by using a castYves Bertot
2018-05-09Merge PR #7438: [gitlab] Do expensive builds with the flambda compiled Coq.Gaëtan Gilbert
2018-05-09Merge PR #7435: [gitlab] Add bleeding-edge flambda build.Gaëtan Gilbert
2018-05-09an example with type classes, but no class inference triggered yetYves Bertot
2018-05-09repackage with an extra ml file, add a usage of new_type_evarYves Bertot
2018-05-09decompose construction of typed term containing evarsYves Bertot
2018-05-09typoYves Bertot
2018-05-09typoYves Bertot
2018-05-09makefile is necessaryYves Bertot
2018-05-09[sphinx] Warn for dangling tacn / cmd / opt / ... references.Clément Pit-Claudel
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-09Replacing a broken reference by hyperlinks in chapter tactics.Hugo Herbelin
2018-05-09A few fixes in chapter tactics.Hugo Herbelin
2018-05-08Merge PR #7459: Try to fix CODEOWNERSThéo Zimmermann
2018-05-08Don't use ref universe_opt_substGaëtan Gilbert
2018-05-08Merge PR #7446: [lib] Re-add `set_timeout` to help users workaround #7408Pierre-Marie Pédrot
2018-05-08intermediary stage with an EConstr containing a hand-made evar, fautyYves Bertot
2018-05-08corrects a problem in documenting how to run the demoYves Bertot
2018-05-08problems with bullet listsYves Bertot
2018-05-08try with triple backticksYves Bertot
2018-05-08attempt to make code inclusions appear correctlyYves Bertot
2018-05-08Try to fix CODEOWNERSMaxime Dénès
2018-05-08[gitlab] Do expensive builds with a flambda-compiled Coq.Emilio Jesus Gallego Arias
Gains seem superior to 50%, but data is taken from Gitlab so no reliable at all.
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
We move syntax for universes from `Misctypes` to `Glob_term`. There is basically no reason that this type is there instead of the proper file, as witnessed by the diff. Unfortunately the change is not compatible due to moving a type to a higher level in the hierarchy, but we expect few problems. This change plus the related PR (#6515) moving universe declaration to their proper place make `Misctypes` into basically an empty file save for introduction patterns.
2018-05-08[CoqProject] Add some comments and remove unnecessary use of Pp.Emilio Jesus Gallego Arias
But indeed we need to split this file, as it is used now from CoqIDE is incorrect.
2018-05-08[coqdep] Remove unnecessary dependency on Pp and CError.Emilio Jesus Gallego Arias
This allows for even earlier bootstrapping.
2018-05-08[coqdep] Minor cleanups.Emilio Jesus Gallego Arias
- Remove inclusion of the `tactics` directory, this is coming from a time loadable modules were found there, now all are under `plugins`. - Remove 2 dependencies so we can bootstrap coqdep earlier. - Use `Format` instead of `Printf` for printing.
2018-05-08[toplevel] Don't ignore output filename provided by user in -oEmilio Jesus Gallego Arias
This was a silly bug introduced in 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly forward the command line option. Thanks to @SkySkimmer for finding out the problem. closes #7447
2018-05-07Merge branch 'master' of https://github.com/ybertot/plugin_tutorialsYves Bertot
2018-05-07adds a copy of the show_proof commandYves Bertot
2018-05-07[gitlab] Add bleeding-edge flambda build.Emilio Jesus Gallego Arias
We also introduce a bit more systematic job naming: `base/edge`. In order to make the flambda switch selectable we update the Docker image so all the dependencies are installed in that one. Note the extra quote rule for the flambda parameters, but unless we can assign arrays to Gitlab variables there is not a good way to do this I'm afraid. With this patch we are getting close to being able to remove most builds from Travis.
2018-05-07[lib] Re-add `set_timeout` to help users workaround #7408Emilio Jesus Gallego Arias
It seems like #7408 will need some potentially intrusive work, so let's add the low-level hook back so third party developments can work well with `8.8.1/master` for the moment.
2018-05-07[vernac] taint two out-of-api `to_constr` use in `comDefinition`.Emilio Jesus Gallego Arias
This should fix #7448 and #7265.
2018-05-07Merge pull request #1 from matejkosik/masterYves Bertot
add some more material (preliminary provided in "tuto2" directory)
2018-05-07Add CODEOWNERS entry for check-owners*.shGaëtan Gilbert
2018-05-07Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging)Maxime Dénès
2018-05-07Merge PR #7371: Propose some updates of the CODEOWNER file.Maxime Dénès
2018-05-07Merge PR #7445: [ci] Add ounit to the base Docker package set.Gaëtan Gilbert
2018-05-07Merge PR #7301: [sphinx] Backport forgotten updates during the migration & ↵Maxime Dénès
other improvements
2018-05-07Merge PR #7440: [ci] Add a default target to `Makefile.ci`Gaëtan Gilbert
2018-05-07fix some detailsMatej Košík
2018-05-07[ci] Add ounit to the base Docker package set.Emilio Jesus Gallego Arias
This should help #6808.
2018-05-07Merge PR #7427: Fix #7413: coqdep warning on repeated filesPierre-Marie Pédrot
2018-05-07fix some detailsMatej Košík
2018-05-07add some more material (preliminary provided in "tuto2" directory)Matej Košík
As it is, it probably need to be edited: (it may be a good idea to drop redundant part; it may be a good idea to make the style of the new information consistent with the already existing material; ...)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 10:27:16 +0000