aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-18Addressing #5434 (ltac pattern-matching refusing to match anonymous variables).Hugo Herbelin
Ltac pattern-matching was requiring dependent variables to be named. This "natural" expectation is however not guaranteed by unification: an evar can be dependent on an anonymous variable, resulting in elaborated terms with dependent anonymous variables (see example in file 5434.v). This commit "fixes" the problem by not requiring that dependent variables are named in ltac pattern-matching. Ltac pattern-matching names itself these anonymous dependent variables, using the same strategy as the printer (i.e. using "H" to display such internally-anonymous dependent variables).
2017-06-15Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]Maxime Dénès
2017-06-15Merge PR#778: Revert "[travis] temporary UniMath overlay"Maxime Dénès
2017-06-15Merge PR#719: Constrexpr.Numeral without bigintMaxime Dénès
2017-06-15Merge PR#769: [lib] Remove obsolete state-management function add_frozen_stateMaxime Dénès
2017-06-15fix dev/base_include (thanks Zimmi48)Pierre Letouzey
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-14Notation.declare_rawnumeral_interpreterPierre Letouzey
This new function is similar to declare_numeral_interpreter, but works on a lower level : instead of bigint, numbers are represented as string of their decimal digits (plus a boolean sign)
2017-06-14G_prim: the bigint entry keeps numbers in raw stringsPierre Letouzey
2017-06-14Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Pierre Letouzey
This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:01:20 +0000