coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing the Value.of_* API for parameterized types.	Pierre-Marie Pédrot	2016-05-04
*	Moving the Val module to Geninterp.	Pierre-Marie Pédrot	2016-05-04
*	Switching to an untyped toplevel representation for Ltac values.	Pierre-Marie Pédrot	2016-05-04
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Remove duplicate declarations.	Guillaume Melquiond	2016-01-02
* \|	Finer-grained types for toplevel values.	Pierre-Marie Pédrot	2015-12-21
* \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Moving the decompose tactic out of the AST.	Pierre-Marie Pédrot	2014-09-01
*	Lazy interpretation of patterns so that expressions such as "intros H H'/H"	Hugo Herbelin	2014-08-18
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Reorganisation of intropattern code	Hugo Herbelin	2014-08-18
*	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack	2014-08-06
*	Faster uconstr.	Arnaud Spiwack	2014-08-01
*	Add a type of untyped term to Ltac's value.	Arnaud Spiwack	2014-07-29
*	Moving wit_unit to Stdarg.	ppedrot	2013-06-19
*	Moving coercion functions out of Tacinterp.	ppedrot	2013-06-12