coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Fixing compilation for 3.12.	Pierre-Marie Pédrot	2015-02-12
*	Tentative fix for bug #4027.	Pierre-Marie Pédrot	2015-02-12
*	Update headers.	Maxime Dénès	2015-01-12
*	Moving the decompose tactic out of the AST.	Pierre-Marie Pédrot	2014-09-01
*	Type-safe version of genarg list / pair / opt functions.	Pierre-Marie Pédrot	2014-08-29
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	Removing "intros untils" from the AST.	Pierre-Marie Pédrot	2014-08-06
*	Faster uconstr.	Arnaud Spiwack	2014-08-01
*	Untyped terms in ltac: simplify [coerce_to_uconstr].	Arnaud Spiwack	2014-08-01
*	Untyped terms in tactic: add the possibility to use a typed term inside an un...	Arnaud Spiwack	2014-07-29
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Expurgating the useless difference between List0 and List1 at the	ppedrot	2013-07-05
*	Removed the distinction between generic Ltac vars and Let/Intro	ppedrot	2013-06-27
*	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot	2013-06-21
*	Moving wit_unit to Stdarg.	ppedrot	2013-06-19
*	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot	2013-06-18
*	Normalizing exception raised by tactic coercions.	ppedrot	2013-06-13
*	Moving coercion functions out of Tacinterp.	ppedrot	2013-06-12