| 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-14 | Merge PR#498: Bignums as a separate opam package | Maxime Dénès | |
| 2017-06-13 | Merge PR#766: Fix ocamldebug for the API | Maxime Dénès | |
| 2017-06-13 | Merge PR#714: Print feature Proof-of-Concept (episode 2) | 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 | Merge PR#718: API cleanup: aliases | 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-12 | Fix ocamldebug for the API | Gaëtan Gilbert | |
| 2017-06-11 | Point ci-hott at a newer version of HoTT | Jason Gross | |
| 2017-06-10 | Remove (useless) aliases from the API. | Matej Košík | |
| 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-07 | Put all plugins behind an "API". | Matej Kosik | |
| 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-05 | Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ↵ | Maxime Dénès | |
| a flag suspectingly renamed in a clearer way | |||
| 2017-06-04 | Added support for a side effect on constants in reduction functions. | Thomas Sibut-Pinote | |
| This exports two functions: - declare_reduction_effect: to declare a hook to be applied when some constant are visited during the execution of some reduction functions (primarily cbv, but also cbn, simpl, hnf, ...). - set_reduction_effect: to declare a constant on which a given effect hook should be called. Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin. Added support for printing effect in functions of tacred.ml. | |||
| 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-06-01 | Merge PR#696: Trunk+cleanup constr of global | Maxime Dénès | |
| 2017-05-31 | Adding overlay for math-comp. | Hugo Herbelin | |
| 2017-05-31 | Creating a module Nameops.Name extending module Names.Name. | Hugo Herbelin | |
| This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name. | |||
| 2017-05-29 | Merge PR#687: Gitlab CI | Maxime Dénès | |
| 2017-05-29 | Cleanup: removal of constr_of_global. | Matthieu Sozeau | |
| Constrintern.pf_global returns a global_reference, not a constr, adapt plugins accordingly, properly registering universes where necessary. | |||
| 2017-05-29 | Merge PR#512: [cleanup] Unify all calls to the error function. | Maxime Dénès | |
| 2017-05-28 | Gitlab CI | Gaëtan Gilbert | |
| 2017-05-27 | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias | |
| This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated. | |||
| 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#637: Short cleaning of the interpretation path for constr_with_bindings | Maxime Dénès | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |