aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-06-18Addressing #5434 (ltac pattern-matching refusing to match anonymous variables).Hugo Herbelin
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
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-15Move Fiat to allowed failures.Maxime Dénès
2017-06-15Remove bedrock from test suite.Maxime Dénès
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
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
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
2017-06-14Makefile.build : cleanup now that micromega.ml isn't generated + sync check o...Pierre Letouzey
2017-06-14Notation.declare_rawnumeral_interpreterPierre Letouzey
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
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
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-26 07:11:05 +0000