| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-09 | A few fixes in chapter tactics. | Hugo Herbelin | |
| 2018-05-08 | Merge PR #7459: Try to fix CODEOWNERS | Théo Zimmermann | |
| 2018-05-08 | Don't use ref universe_opt_subst | Gaëtan Gilbert | |
| 2018-05-08 | Merge PR #7446: [lib] Re-add `set_timeout` to help users workaround #7408 | Pierre-Marie Pédrot | |
| 2018-05-08 | intermediary stage with an EConstr containing a hand-made evar, fauty | Yves Bertot | |
| 2018-05-08 | corrects a problem in documenting how to run the demo | Yves Bertot | |
| 2018-05-08 | problems with bullet lists | Yves Bertot | |
| 2018-05-08 | try with triple backticks | Yves Bertot | |
| 2018-05-08 | attempt to make code inclusions appear correctly | Yves Bertot | |
| 2018-05-08 | Try to fix CODEOWNERS | Maxime 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 -o | Emilio 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-07 | Merge branch 'master' of https://github.com/ybertot/plugin_tutorials | Yves Bertot | |
| 2018-05-07 | adds a copy of the show_proof command | Yves 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 #7408 | Emilio 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-07 | Merge pull request #1 from matejkosik/master | Yves Bertot | |
| add some more material (preliminary provided in "tuto2" directory) | |||
| 2018-05-07 | Add CODEOWNERS entry for check-owners*.sh | Gaëtan Gilbert | |
| 2018-05-07 | Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging) | Maxime Dénès | |
| 2018-05-07 | Merge PR #7371: Propose some updates of the CODEOWNER file. | Maxime Dénès | |
| 2018-05-07 | Merge PR #7445: [ci] Add ounit to the base Docker package set. | Gaëtan Gilbert | |
| 2018-05-07 | Merge PR #7301: [sphinx] Backport forgotten updates during the migration & ↵ | Maxime Dénès | |
| other improvements | |||
| 2018-05-07 | Merge PR #7440: [ci] Add a default target to `Makefile.ci` | Gaëtan Gilbert | |
| 2018-05-07 | fix some details | Matej Košík | |
| 2018-05-07 | [ci] Add ounit to the base Docker package set. | Emilio Jesus Gallego Arias | |
| This should help #6808. | |||
| 2018-05-07 | Merge PR #7427: Fix #7413: coqdep warning on repeated files | Pierre-Marie Pédrot | |
| 2018-05-07 | fix some details | Matej Košík | |
| 2018-05-07 | add 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; ...) | |||
| 2018-05-06 | Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CI | Gaëtan Gilbert | |
| 2018-05-06 | Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow ↵ | Maxime Dénès | |
| kernel style. | |||
| 2018-05-06 | [ci] Add a default target to `Makefile.ci` | Emilio Jesus Gallego Arias | |
| So we avoid problems like the one in #7438. | |||
| 2018-05-05 | [gitlab] [circleci] Use a Custom Docker Image as base CI setup. | Emilio Jesus Gallego Arias | |
| We provide a custom `Dockerfile` for Coq's CI system, based on `ubuntu:bionic`. The image includes the required set of packages and OPAM switches. This greatly simplifies the Gitlab and Circle scripts, at the cost of having to push a Docker build for them to depend on. Travis is not included in this PR as it requires significant more refactoring due to lack of native Docker support. This is work in progress but ready, a build hook is used so the image is properly tagged in the Docker autobuilder. We need to improve the autobuilder setup but this last point requires some design on how to trigger it. Fixes #7383 | |||
| 2018-05-05 | [sphinx] Fixes around apply, including indentation and fixing a Coq warning. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Fixes around refine, including indentation and a hard-coded ref. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Improve typeclass chapter. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Add indices for only, all and par. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Improvements around injection tactic. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Improve part about Hints. | Théo Zimmermann | |
| Fix Hint (Transparent | Opaque) index. | |||
| 2018-05-05 | [sphinx] Re-indent to get much better rendering. | Théo Zimmermann | |
| Add some more cmd references. And use deprecated directives. | |||
| 2018-05-05 | Remove duplicate Introduction title. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Backport changes from #5979. | Théo Zimmermann | |
| 2018-05-05 | Two more uses of verbatim in doc. | Théo Zimmermann | |
| 2018-05-05 | Clean-up around cmd documentation. | Théo Zimmermann | |
| In particular, remove trailing dots. | |||
| 2018-05-05 | Remove duplicate Extraction commands documentation. | Théo Zimmermann | |
| 2018-05-05 | Add some refs in the Omega chapter. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |