| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-14 | [travis] overlay for fiat-crypto (a Require Import FunInd) | Pierre Letouzey | |
| 2017-06-14 | [travis] overlays for CompCert and VST (an extra Require Export FunInd) | Pierre Letouzey | |
| 2017-06-14 | [travis] fix Software Foundation (one added Require Extraction) | Pierre Letouzey | |
| 2017-06-14 | [travis] fix CoLoR by inserting some Require Import FunInd | Pierre Letouzey | |
| 2017-06-14 | Temporary overlays for bignums. | Maxime Dénès | |
| 2017-06-13 | [travis] overlay for corn | Pierre Letouzey | |
| 2017-06-13 | [travis] extra test ci-bignums (+factorize other scripts) | Pierre Letouzey | |
| 2017-06-13 | [travis] overlay + extra deps for math-classes (and formal-topology) | Pierre Letouzey | |
| 2017-06-13 | [travis] adapt CoLoR compilation to depend on the bignum package | Pierre Letouzey | |
| 2017-06-13 | Merge PR#764: Point ci-hott at a newer version of HoTT | Maxime Dénès | |
| 2017-06-12 | Merge PR#715: Add coq-dpdgraph ci | Maxime Dénès | |
| 2017-06-12 | Temporary overlay, waiting for upstream PR merges. | Maxime Dénès | |
| 2017-06-12 | add overlays | Matej Košík | |
| 2017-06-11 | Point ci-hott at a newer version of HoTT | Jason Gross | |
| 2017-06-08 | Mirror dpdgraph's travis test more accurately | Jason Gross | |
| 2017-06-08 | Remove coq-dpdgraph overlay | Jason Gross | |
| 2017-06-08 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-06-08 | Remove overlay. | Maxime Dénès | |
| 2017-06-07 | add overlays | Matej Košík | |
| 2017-06-06 | Overlay. | Maxime Dénès | |
| 2017-06-06 | Remove some overlays. | Maxime Dénès | |
| 2017-06-06 | Overlays. | Maxime Dénès | |
| 2017-06-06 | Merge PR#723: [travis] [fiat] Test also fiat-core. | Maxime Dénès | |
| 2017-06-02 | Add an overlay for coq-dpdgraph for 8.7 | Jason Gross | |
| 2017-06-02 | Add coq-dpdgraph CI | Jason Gross | |
| 2017-06-02 | [travis] [fiat] Test also fiat-core. | Emilio Jesus Gallego Arias | |
| I didn't rename the test file to `fiat` as IMHO it is not worth the noise. | |||
| 2017-05-31 | Adding overlay for math-comp. | Hugo Herbelin | |
| 2017-05-29 | Merge PR#687: Gitlab CI | Maxime Dénès | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |