coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
*	Fix bugs	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Make unification use subtyping info of inductives	Amin Timany	2017-06-16
*	Fix cum/conv for inductive types	Amin Timany	2017-06-16
*	Use inductive subtyping for conv/cumul	Amin Timany	2017-06-16
*	Change the place of inference after sect discharge	Amin Timany	2017-06-16
*	Subtyping inference for inductoves and records	Amin Timany	2017-06-16
*	Add subtyping inference for inductive types	Amin Timany	2017-06-16
*	Correct subtyping check for constructors	Amin Timany	2017-06-16
*	Fix typo in error message	Amin Timany	2017-06-16
*	Check subtyping of inductive types in Kernel	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	New datastructure for universes of inductive types	Amin Timany	2017-06-16
*	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	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