Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge PR#375: Deprecation | Maxime Dénès | 2017-06-15 |
|\ | |||
* | | Move Fiat to allowed failures. | Maxime Dénès | 2017-06-15 |
| | | | | | | | | For now, Fiat still relies on 8.4 compatibility. | ||
* | | Remove bedrock from test suite. | Maxime Dénès | 2017-06-15 |
| | | | | | | | | | | | | 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. | ||
* | | Remove dependency on -compat flag in coq_makefile test suite. | Maxime Dénès | 2017-06-15 |
| | | |||
* | | Merge PR#749: Normalize deprecation notices of ./configure | Maxime Dénès | 2017-06-14 |
|\ \ | |||
* \ \ | Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations). | Maxime Dénès | 2017-06-14 |
|\ \ \ | |||
* \ \ \ | Merge PR#758: [toplevel] Print error header on fatal batch error. | Maxime Dénès | 2017-06-14 |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#763: [proof] Deprecate redundant wrappers. | Maxime Dénès | 2017-06-14 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#765: Remove obsolete Show commands | Maxime Dénès | 2017-06-14 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR#739: completing a sentence in a comment | Maxime Dénès | 2017-06-14 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613 | Maxime Dénès | 2017-06-14 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match"). | Maxime Dénès | 2017-06-14 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR#673: Two fixes about zify (bugs #5336 and #5439) | Maxime Dénès | 2017-06-14 |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#448: Do not recompute twice the whnf of terms in conversion. | 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#703: New version of the selective-unfolding PR | Maxime Dénès | 2017-06-14 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58 | Maxime Dénès | 2017-06-14 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | | | | | | [print] Allow Selective Printing of Notations | Emilio Jesus Gallego Arias | 2017-06-14 |
| |/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We add new API to the printer to allows toggling the printing of individual notations and scopes: ```ocaml val toggle_scope_printing : scope:Notation_term.scope_name -> activate:bool -> unit val toggle_notation_printing : ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit ``` This API is meant to be used by ML plugins. [this commit includes some refactoring by EJGA] | ||
* | | | | | | | | | | | | | | Temporary overlays because fewer plugins are loaded at startup. | Maxime Dénès | 2017-06-14 |
| | | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | Merge PR#220: Less init plugins | 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 |
| | | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | Recdef do now a Require Export FunInd (better compat) | Pierre Letouzey | 2017-06-14 |
| | | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | Grammar hacks to get nice errors about non-loaded plugins (extr,recdef) | Pierre Letouzey | 2017-06-14 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since previous commit, some plugins are not loaded initially anymore : extraction, funind. To ease this transition toward a mandatory Require, we hack here the vernac grammar in order to get customized error messages telling what to Require instead of the dreadful "Illegal begin of vernac". Normally, these fake grammar entries are overloaded later by the grammar extensions in these plugins. This code is meant to be removed in a few releases, when this transition is considered finished. NB : In a first attempt, a similar trick was tried in g_tactics.ml4 to provide customized error message for "functional induction" and "functional inversion", but this was leading to anomalies. | ||
| * | | | | | | | | | | | | | | API: exports Mltop.module_is_known to both API.mli and grammar_API.mli | Pierre Letouzey | 2017-06-14 |
| | | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey | 2017-06-14 |
|/ / / / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted. | ||
* | | | | | | | | | | | | | | Makefile.build : cleanup now that micromega.ml isn't generated + sync check ↵ | Pierre Letouzey | 2017-06-14 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | of this file There is now a warning if the content of micromega.ml isn't what MExtraction.v would produce. | ||
| | | | | | | | | | | | | * | Remove deprecated options from the standard library. | Guillaume Melquiond | 2017-06-14 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Deprecate options that were introduced for compatibility with 8.4. | Guillaume Melquiond | 2017-06-14 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Deprecate options that were introduced for compatibility with 8.2. | Guillaume Melquiond | 2017-06-14 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Remove options deprecated since 8.4. | Guillaume Melquiond | 2017-06-14 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Add support for Coq 8.6. | Guillaume Melquiond | 2017-06-14 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Remove support for Coq 8.4. | Guillaume Melquiond | 2017-06-14 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Remove support for Coq 8.3. | Guillaume Melquiond | 2017-06-14 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Remove support for Coq 8.2. | Guillaume Melquiond | 2017-06-14 |
| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | Add a version to be used when parsing compatibility notations mentioning old ↵ | Guillaume Melquiond | 2017-06-14 |
| |_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | versions. | ||
* | | | | | | | | | | | | | 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-14 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | | | | Makefile.build: do *not* build PLUGINSCMO by default (followup of PR #709) | Pierre Letouzey | 2017-06-13 |
| | | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | Merge PR#385: Equality of sigma types | 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 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | | | | | | | | 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 |
| | | | | | | | | | | | | | | | | | |||
* | | | | | | | | | | | | | | | | | Merge PR#757: Better sectioning on travis log printing in test-suite | Maxime Dénès | 2017-06-13 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | * | | | | | | | | | | | Documenting the change of default flag value of Refine.refine. | Pierre-Marie Pédrot | 2017-06-13 |
| | | | | | | | | | | | | | | | | | |