coq - The formal proof system

Age	Commit message (Expand)	Author
2016-05-04	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-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-02	Remove duplicate declarations.	Guillaume Melquiond
2015-12-21	Finer-grained types for toplevel values.	Pierre-Marie Pédrot
2015-12-21	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-09-01	Moving the decompose tactic out of the AST.	Pierre-Marie Pédrot
2014-08-18	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-06	[uconstr]: use a closure instead of eager substitution.	Arnaud Spiwack
2014-08-01	Faster uconstr.	Arnaud Spiwack
2014-07-29	Add a type of untyped term to Ltac's value.	Arnaud Spiwack
2013-06-19	Moving wit_unit to Stdarg.	ppedrot
2013-06-12	Moving coercion functions out of Tacinterp.	ppedrot