| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-28 | Gitlab CI | Gaëtan Gilbert | |
| 2017-05-27 | [coqlib] Move `Coqlib` to `library/`. | Emilio Jesus Gallego Arias | |
| We move Coqlib to library in preparation for the late binding of Gallina-level references. Placing `Coqlib` in `library/` is convenient as some components such as pretyping need to depend on it. By moving we lose the ability to locate references by syntactic abbreviations, but IMHO it makes to require ML code to refer to a true constant instead of an abbreviation/notation. Unfortunately this change means that we break the `Coqlib` API (providing a compatibility function is not possible), however we do so for a good reason. The main changes are: - move `Coqlib` to `library/`. - remove reference -> term from `Coqlib`. In particular, clients will have different needs with regards to universes/evar_maps, so we force them to call the (not very safe) `Universes.constr_of_global` explicitly so the users are marked. - move late binding of impossible case from `Termops` to `pretying/Evarconv`. Remove hook. - `Coqlib.find_reference` doesn't support syntactic abbreviations anymore. - remove duplication of `Coqlib` code in `Program`. - remove duplication of `Coqlib` code in `Ltac.Rewrite`. - A special note about bug 5066 and commit 6e87877 . This case illustrates the danger of duplication in the code base; the solution chosen there was to transform the not-found anomaly into an error message, however the general policy was far from clear. The long term solution is indeed make `find_reference` emit `Not_found` and let the client handle the error maybe non-fatally. (so they can test for constants. | |||
| 2017-05-27 | [travis] temporary UniMath overlay | Maxime Dénès | |
| We are waiting for an upstream merge of a fix related to coq_makefile2. | |||
| 2017-05-25 | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | |
| 2017-05-25 | Merge PR#406: coq makefile2 | Maxime Dénès | |
| 2017-05-25 | [location] [travis] Add overlays for located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | |
| Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers. | |||
| 2017-05-23 | Add parsers-examples target to fiat-parsers ci | Jason Gross | |
| This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build. | |||
| 2017-05-23 | overlay for UniMath | Enrico Tassi | |
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-05-10 | Switch bedrock to mit-plv base | Jason Gross | |
| 2017-05-01 | Add bmsherman/topology to the ci | Jason Gross | |
| This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk. | |||
| 2017-04-27 | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès | |
| 2017-04-27 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-04-25 | [travis] mathcomp and fiat overlay for #402 | Emilio Jesus Gallego Arias | |
| 2017-04-24 | Adding a dedicated travis overlay for fiat-parsers. | Pierre-Marie Pédrot | |
| 2017-04-20 | Add bedrock targets src and facade | Jason Gross | |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès | |
| 2017-04-14 | [travis] Use the lite target for fiat-crypto. | Maxime Dénès | |
| 2017-04-07 | [travis] Overlay for PR#461: Camlp4 removal. | Emilio Jesus Gallego Arias | |
| 2017-03-24 | [travis] Backport from trunk: VST | Emilio Jesus Gallego Arias | |
| 2017-03-24 | [travis] Add VST | Emilio Jesus Gallego Arias | |
| 2017-03-22 | [travis] Fix iris-coq build. | Emilio Jesus Gallego Arias | |
| We need to do a bit of hacking, but it should be fine for the short term. c.f. https://gitlab.mpi-sws.org/FP/iris-coq/issues/83 | |||
| 2017-03-22 | [travis] [8.6.only] Backport latest changes from trunk. | Emilio Jesus Gallego Arias | |
| 2017-03-21 | trivial: fix comment | Matej Kosik | |
| 2017-03-13 | [travis] Basic support for overlays. | Emilio Jesus Gallego Arias | |
| We now allow the user to overlay contribution repositories and branches by adding their own rules to `ci-basic-overlay.sh`. This just provides very basic support. | |||
| 2017-03-10 | [travis] Make the git_checkout function more reliable. | Théo Zimmermann | |
| This commit also documents the behavior of said function; and fix the location of the ssreflect clone to an absolute path (this is now necessary). | |||
| 2017-03-10 | [travis] Adding a template file and using it for all targets. | Théo Zimmermann | |
| 2017-03-10 | [travis] Change headband for wider compatibility. | Théo Zimmermann | |
| 2017-03-10 | Improve build of travis target on local machine. | Théo Zimmermann | |
| - Move the git clones to a specific subfolder to avoid pollution. - Do not fail when git clone already exist (but make sure it is up-to-date). | |||
| 2017-03-10 | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | |
| We need to agree a bit more with upstream. | |||
| 2017-03-09 | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | |
| We need to agree a bit more with upstream. | |||
| 2017-03-02 | [travis] Backport trunk's travis support. | Emilio Jesus Gallego Arias | |
| 2017-02-24 | [travis] [External CI] fiat-parsers | Emilio Jesus Gallego Arias | |
| 2017-02-21 | [travis] track an 8.7 specific branch of HoTT. | Maxime Dénès | |
| This is required since we merged PR#309: Ltac as a plugin. | |||
| 2017-02-15 | [travis] [External CI] CompCert official 8.6 support + UniMath | Emilio Jesus Gallego Arias | |
| 2017-02-15 | [travis] [External CI] Factor out math-comp installs. | Emilio Jesus Gallego Arias | |
| We make math-comp overlays easier, we also start structuring the scripts a bit more. | |||
| 2017-02-07 | Merge PR#425: [travis] [External CI] [geocoq] don't build slow file | Maxime Dénès | |
| 2017-02-07 | [travis] [External CI] [geocoq] don't build slow file | Emilio Jesus Gallego Arias | |
| Unfortunately `Ch16_coordinates_with_functions.v` takes alone ~15 minutes which is too much for Travis. Pity, because it was a nice use case. | |||
| 2017-02-07 | [travis] [External CI] iris-coq: fix dependencies | Emilio Jesus Gallego Arias | |
| 2017-02-07 | [travis] [External CI] GeoCoq | Emilio Jesus Gallego Arias | |
| 2017-02-07 | [travis] Move ci files from `tools` to `dev`. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |