coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| * \| \| \|	Extend definition of inductives to include subtyping info	Amin Timany	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
* \| \| \| \| \| \| \| \| \| \|	Merge PR#375: Deprecation	Maxime Dénès	2017-06-15
\|\ \ \ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \| \| \|	Move Fiat to allowed failures.	Maxime Dénès	2017-06-15
* \| \| \| \| \| \| \| \| \| \| \|	Remove bedrock from test suite.	Maxime Dénès	2017-06-15
* \| \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	[typeclasses eauto] Fix bug #3943: non-termination in topological	Matthieu Sozeau	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
\| \|/ / / / / / / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\|/ / / / / / / / / / / / / / / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Makefile.build : cleanup now that micromega.ml isn't generated + sync check o...	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	API additions for coq-dpdgraph	Gaëtan Gilbert	2017-06-14
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Notation.declare_rawnumeral_interpreter	Pierre Letouzey	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \|	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
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|