| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-15 | Merge PR#778: Revert "[travis] temporary UniMath overlay" | Maxime Dénès | |
| 2017-06-15 | fix dev/base_include (thanks Zimmi48) | Pierre Letouzey | |
| 2017-06-15 | Remove bedrock from test suite. | Maxime Dénès | |
| Bedrock relies on the 8.4 compat flag that we are removing, and we heard from MIT that they did not plan to port bedrock to more recent versions of Coq. | |||
| 2017-06-14 | Merge PR#749: Normalize deprecation notices of ./configure | Maxime Dénès | |
| 2017-06-14 | Merge PR#622: Change the default flag value for Refine.refine | Maxime Dénès | |
| 2017-06-14 | Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58 | Maxime Dénès | |
| 2017-06-14 | Temporary overlays because fewer plugins are loaded at startup. | Maxime Dénès | |
| 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 | Revert "[travis] temporary UniMath overlay" | Théo Zimmermann | |
| This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged. | |||
| 2017-06-13 | Merge PR#714: Print feature Proof-of-Concept (episode 2) | Maxime Dénès | |
| 2017-06-13 | Dualize the unsafe flag of refine into typecheck and make it mandatory. | Pierre-Marie Pédrot | |
| 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 | Documenting the change of default flag value of Refine.refine. | Pierre-Marie Pédrot | |
| 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 | [travis overlay] Partially Revert 013c0232953f1f58 | Jason Gross | |
| I've pushed commits which add `-bypass-API` to bedrock in the proper way, so these overlays are no longer needed | |||
| 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-11 | Normalize deprecation notices of ./configure | Théo Zimmermann | |
| Always output a warning on stderr when a deprecated option is used. | |||
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |