aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-14Direct link to Travis branch builds.Théo Zimmermann
2017-06-14[typeclasses eauto] Fix bug #3943: non-termination in topologicalMatthieu Sozeau
sorting for the dependency order option.
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-14API additions for coq-dpdgraphGaëtan Gilbert
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-13Merge remote-tracking branch 'upstream/trunk' into trunkWilliam Lawvere
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-13Remove some useless code in Term_typingGaëtan Gilbert
The [let _typ = ...] comes from before universe polymorphism. In those times it was [let _typ, cst = ...] which produced something of use. The asserts come from 359e4ffe3 and before (2006 and before). In those times [Typeops.infer] rebuilt the term being typed, but nowadays the assert seems of little use.
2017-06-13doc: improve grammar of RefMan-synWilliam Lawvere
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-13Revert "[travis] temporary UniMath overlay"Théo Zimmermann
This reverts commit 7ca4e36af8a12236a618bd3a8d045439df40dd43. Not necessary anymore since UniMath/UniMath#715 has been merged.
2017-06-13Improving documentation of tactic "move" (report #4561).Hugo Herbelin
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 12:13:00 +0000