coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
\| \| \| \| \| \| \|	Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead.
*	Remove the last use of the low-level Proof_type API in ssr.	Pierre-Marie Pédrot	2017-06-16
\|
*	Merge PR#748: [stm] More fixes for nested commands [bugzilla 5589]	Maxime Dénès	2017-06-15
\|\
* \	Merge PR#778: Revert "[travis] temporary UniMath overlay"	Maxime Dénès	2017-06-15
\|\ \
* \ \	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\ \ \
* \ \ \	Merge PR#769: [lib] Remove obsolete state-management function add_frozen_state	Maxime Dénès	2017-06-15
\|\ \ \ \
* \| \| \| \|	fix dev/base_include (thanks Zimmi48)	Pierre Letouzey	2017-06-15
\| \| \| \| \|
* \| \| \| \|	Makefile.build : restore (temporarily?) the anti-cmi-corruption hacks	Pierre Letouzey	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
* \| \| \| \|	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.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Notation.declare_rawnumeral_interpreter	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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)
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	G_prim: the bigint entry keeps numbers in raw strings	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey	2017-06-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|