aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-15Remove ci-fiat-parsers from allowed_failuresJason Gross
It shouldn't be failing.
2017-06-15Update fiat-parsers overlayJason Gross
2017-06-15API: Hints.run_hint,Pfedit.current_proof_statementJason Gross
Add them for fiat-parsers
2017-06-15Makefile.build : restore (temporarily?) the anti-cmi-corruption hacksPierre Letouzey
Due to the recent conversion of many .mli-only files into .ml files (hugely debatable impact of the API introduction), parallel make may fail badly again (always the same race between ocamlc and ocamlopt for .cmi). Still working on a proper fix, but meanwhile let's reintroduce the old hacks against these corruptions.
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-15Move Fiat to allowed failures.Maxime Dénès
For now, Fiat still relies on 8.4 compatibility.
2017-06-15Remove 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-15Remove dependency on -compat flag in coq_makefile test suite.Maxime Dénès
2017-06-14Merge PR#749: Normalize deprecation notices of ./configureMaxime Dénès
2017-06-14Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Maxime Dénès
2017-06-14Merge PR#758: [toplevel] Print error header on fatal batch error.Maxime Dénès
2017-06-14Merge PR#763: [proof] Deprecate redundant wrappers.Maxime Dénès
2017-06-14Merge PR#765: Remove obsolete Show commandsMaxime Dénès
2017-06-14Merge PR#739: completing a sentence in a commentMaxime Dénès
2017-06-14Merge PR#738: [kernel] Improve proof using message, fixes bugzilla #3613Maxime Dénès
2017-06-14Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Maxime Dénès
2017-06-14Merge PR#673: Two fixes about zify (bugs #5336 and #5439)Maxime Dénès
2017-06-14Merge PR#448: Do not recompute twice the whnf of terms in conversion.Maxime Dénès
2017-06-14Merge PR#622: Change the default flag value for Refine.refineMaxime Dénès
2017-06-14Merge PR#703: New version of the selective-unfolding PRMaxime Dénès
2017-06-14Merge PR#771: [travis overlay] Partially Revert 013c0232953f1f58Maxime Dénès
2017-06-14[print] Allow Selective Printing of NotationsEmilio Jesus Gallego Arias
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]
2017-06-14Temporary overlays because fewer plugins are loaded at startup.Maxime Dénès
2017-06-14Merge PR#220: Less init pluginsMaxime 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 FunIndPierre Letouzey
2017-06-14Recdef do now a Require Export FunInd (better compat)Pierre Letouzey
2017-06-14Grammar hacks to get nice errors about non-loaded plugins (extr,recdef)Pierre Letouzey
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.
2017-06-14API: exports Mltop.module_is_known to both API.mli and grammar_API.mliPierre Letouzey
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
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.
2017-06-14Makefile.build : cleanup now that micromega.ml isn't generated + sync check ↵Pierre Letouzey
of this file There is now a warning if the content of micromega.ml isn't what MExtraction.v would produce.
2017-06-14Remove deprecated options from the standard library.Guillaume Melquiond
2017-06-14Deprecate options that were introduced for compatibility with 8.4.Guillaume Melquiond
2017-06-14Deprecate options that were introduced for compatibility with 8.2.Guillaume Melquiond
2017-06-14Remove options deprecated since 8.4.Guillaume Melquiond
2017-06-14Add support for Coq 8.6.Guillaume Melquiond
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-14Remove support for Coq 8.3.Guillaume Melquiond
2017-06-14Remove support for Coq 8.2.Guillaume Melquiond
2017-06-14Add a version to be used when parsing compatibility notations mentioning old ↵Guillaume Melquiond
versions.
2017-06-14Temporary overlays for bignums.Maxime Dénès
2017-06-14Merge PR#498: Bignums as a separate opam packageMaxime Dénès
2017-06-13Makefile.build: do *not* build PLUGINSCMO by default (followup of PR #709)Pierre Letouzey
2017-06-13Merge PR#385: Equality of sigma typesMaxime Dénès
2017-06-13Merge PR#766: Fix ocamldebug for the APIMaxime Dénès
2017-06-13Merge PR#714: Print feature Proof-of-Concept (episode 2)Maxime Dénès
2017-06-13Dualize the unsafe flag of refine into typecheck and make it mandatory.Pierre-Marie Pédrot
2017-06-13[travis] overlay for cornPierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 06:53:05 +0000