coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Delayed weak constraints for cumulative inductive types.	Gaëtan Gilbert	2018-03-09
*	Statically enforce that ULub is only between levels.	Gaëtan Gilbert	2018-03-09
*	Option for messing with inference of irrelevant constraints	Gaëtan Gilbert	2018-03-09
*	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
*	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
*	Merge PR #6895: [compat] Remove "Refolding Reduction" option.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6747: Relax conversion of constructors according to the pCuIC model	Maxime Dénès	2018-03-09
\|\ \
* \ \	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\ \ \
\| \| \| *	[compat] Remove "Refolding Reduction" option.	Emilio Jesus Gallego Arias	2018-03-08
\| \|_\|/ \|/\| \|
\| \| *	Leave cumul constructor universes as is during unif	Matthieu Sozeau	2018-03-08
\| \| *	Relax conversion of constructors according to the pCuIC model	Matthieu Sozeau	2018-03-08
\| \|/ \|/\|
* \|	Merge PR #6905: Fix make ml-doc	Maxime Dénès	2018-03-07
\|\ \
* \ \	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\ \ \
\| \| \| *	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6900: [compat] Remove "Tactic Pattern Unification"	Maxime Dénès	2018-03-06
\|\ \ \
\| \| \| *	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
\| \|_\|/ \|/\| \|
\| \| *	Allow universe declarations for [with Definition].	Gaëtan Gilbert	2018-03-05
* \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \
* \ \ \	Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad	Maxime Dénès	2018-03-05
\|\ \ \ \
* \ \ \ \	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| * \| \|	reductionops: remove dead code "bind_assum"	Enrico Tassi	2018-03-04
* \| \| \| \|	Merge PR #6791: Removing compatibility support for versions older than 8.5.	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\ \ \ \ \
\| \| \| * \| \|	Handling evars in the VM.	Pierre-Marie Pédrot	2018-03-03
\| \| \| \| \| *	[compat] Remove "Tactic Pattern Unification"	Emilio Jesus Gallego Arias	2018-03-03
\| \| \| \| \|/ \| \| \| \|/\|
\| \| * \| \|	Remove 8.5 compatibility support.	Théo Zimmermann	2018-03-02
\| \| * \| \|	Remove VOld compatibility flag.	Théo Zimmermann	2018-03-02
\| \| \|/ /
* \| / /	[VM] Unify Const_sorts and Const_type, and remove Vsort.	Maxime Dénès	2018-03-02
\| \|/ / \|/\| \|
\| * \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\|/ /
* \|	comment "resolvability" bit in Evd.evar_map	Enrico Tassi	2018-02-27
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Maxime Dénès	2018-02-24
\|\
* \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
* \|	Merge PR #6767: [ci] add elpi	Maxime Dénès	2018-02-21
\|\ \
\| \| *	Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Hugo Herbelin	2018-02-20
* \| \|	Using an "as" clause when needed for printing irrefutable patterns.	Hugo Herbelin	2018-02-20
* \| \|	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
* \| \|	Canonically add an encoding in glob_constr of "as" operator for cases_pattern.	Hugo Herbelin	2018-02-20
* \| \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
\| \|/ \|/\|
\| *	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
\|/
*	Merge PR #6759: detype_case predicate is not optional	Maxime Dénès	2018-02-19
\|\
* \|	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert	2018-02-16
* \|	Fix reduction flags in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| *	detype_case predicate is not optional	Gaëtan Gilbert	2018-02-14
\|/
*	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\
* \	Merge PR #6128: Simplification: cumulativity information is variance informa...	Maxime Dénès	2018-02-12
\|\ \
* \ \	Merge PR #6418: More detailed error messages for Canonical Structure, #6398	Maxime Dénès	2018-02-12
\|\ \ \
* \ \ \	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\ \ \ \
\| \| \| * \|	inferCumulativity: add comment to explain [if not is_arity].	Gaëtan Gilbert	2018-02-11
\| \| \| * \|	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11