coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	checker Indtypes: remove unused arguments	Gaëtan Gilbert	2018-07-03
*	checker Modops strengthening: remove unused argument resolver	Gaëtan Gilbert	2018-07-03
*	Subtyping.check_constant: remove unused module path argument.	Gaëtan Gilbert	2018-07-03
*	Inductive.extract_stack,filter_stack_domain: remove unused arguments	Gaëtan Gilbert	2018-07-03
*	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
*	Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...	Matthieu Sozeau	2018-06-25
\|\
* \|	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
* \|	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot	2018-06-23
\| *	Remove hack skipping comparison of algebraic universes in subtyping.	Gaëtan Gilbert	2018-06-22
\| *	Remove enforce_leq from checker	Gaëtan Gilbert	2018-06-21
\|/
*	Merge PR #7841: Remove Canary	Pierre-Marie Pédrot	2018-06-19
\|\
\| *	Remove Canary.	whitequark	2018-06-18
* \|	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot	2018-06-17
* \|	Remove the proj_eta field of the kernel.	Pierre-Marie Pédrot	2018-06-17
* \|	Getting rid of the const_proj field in the kernel.	Pierre-Marie Pédrot	2018-06-17
\|/
*	Fix the checker by merely adapting the data structure.	Pierre-Marie Pédrot	2018-06-07
*	Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...	Matthieu Sozeau	2018-06-04
\|\
* \|	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
* \|	Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in glob...	Pierre-Marie Pédrot	2018-05-25
\|\ \
* \ \	Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...	Pierre-Marie Pédrot	2018-05-24
\|\ \ \
\| \| * \|	Fix #7323: coqchk puts polymorphic univs of inductive in global env	Gaëtan Gilbert	2018-05-24
\| \|/ / \|/\| \|
* \| \|	Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants	Pierre-Marie Pédrot	2018-05-24
\|\ \ \
* \ \ \	Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...	Pierre-Marie Pédrot	2018-05-24
\|\ \ \ \
\| \| \| * \|	Moving Rtree.smart_map into Rtree.Smart.map.	Hugo Herbelin	2018-05-23
\| \| \| * \|	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
\| \| \| * \|	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
\| \| \| * \|	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
\| \|_\|/ / \|/\| \| \|
\| \| \| *	Fix #7539: Checker does not properly handle negative coinductive types.	Pierre-Marie Pédrot	2018-05-18
* \| \| \|	Infrastructure for ocamldebug on the checker	Gaëtan Gilbert	2018-05-13
\| \|_\|/ \|/\| \|
\| \| *	Fix #7327: coqchk subtyping of polymorphic constants	Gaëtan Gilbert	2018-04-23
\| \|/
\| *	Fix #6798: coqchk ignores ugraph when comparing constant instances	Gaëtan Gilbert	2018-04-20
\|/
*	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
*	Merge PR #6800: [checker] Printer cleanup.	Maxime Dénès	2018-03-09
\|\
* \|	Update checker to reflect rule on constructors of polymorphic inductive types	Matthieu Sozeau	2018-03-08
\| *	[checker] Printer cleanup.	Emilio Jesus Gallego Arias	2018-03-07
\|/
*	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \	Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)	Maxime Dénès	2018-02-28
\|\ \
\| \| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| \|/ \|/\|
* \|	Merge PR #6740: Adding a sanity check on inductive variance subtyping.	Maxime Dénès	2018-02-21
\|\ \
* \ \	Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...	Maxime Dénès	2018-02-19
\|\ \ \
* \ \ \	Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...	Maxime Dénès	2018-02-19
\|\ \ \ \
\| * \| \| \|	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| * \| \|	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
\| \|/ / / \|/\| \| \|
\| \| * \|	Adding a sanity check on inductive variance subtyping.	Pierre-Marie Pédrot	2018-02-15
\| \|/ / \|/\| \|
* \| \|	Merge PR #6262: [error] Replace msg_error by a proper exception.	Maxime Dénès	2018-02-12
\|\ \ \
\| \| \| *	dest_{prod,lam}: no Cast case (it's removed by whd)	Gaëtan Gilbert	2018-02-11
\| \| \|/
* \| /	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
\| \|/ \|/\|
\| *	[error] Replace msg_error by a proper exception.	Emilio Jesus Gallego Arias	2018-02-09
\|/
*	checker: cleanup projection unfolding	Gaëtan Gilbert	2018-02-02