coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	use map_constr more efficiently	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Optimization	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Use a smart map_constr	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Move (part of) tests from checker to success	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove Warnings: unused value ...	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Checker add test for non-trivial constraints	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Properly instantiate contexts before pushing	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Enable the checking of ind subtyping in checker	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Document cumulativity for inductive types	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Change the option to Set Inductive Cumulativity	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add printing of cumulativity in inductive types	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Move univops from kernel to library	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Correct coqchk checking subtyping relation for inductives	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Correct coqchk reduction	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Simplify Univ.ml	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix a bug	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Disable debug printing	Amin Timany	2017-06-16
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Move TIMER to right in front of COQC	Jason Gross	2017-06-15
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Fix `make TIMED=1` garbage	Jason Gross	2017-06-15
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \|	Strip trailing whitespace	Jason Gross	2017-06-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \|	Merge PR#741: Fix documentation of Typeclasses eauto :=	Maxime Dénès	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \ \ \ \ \ \	Merge PR#713: Bump year in headers.	Maxime Dénès	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \ \ \ \ \ \ \	Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints	Maxime Dénès	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \ \ \ \ \ \ \ \	Merge PR#752: Adding a test case as requested in bug 5205.	Maxime Dénès	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| * \ \ \ \ \ \ \ \ \	Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module imports	Maxime Dénès	2017-06-15
\| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \|_\|_\|_\|_\|_\|_\|/ / / \| \| \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \|	plugins/ltac : avoid spurious .cmxs files	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