coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Typeclasses:rename solve_instantiation* & use Hook	Matthieu Sozeau	2016-06-16
*	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
*	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau	2016-06-16
*	Typeclasses: refine the eauto tactic	Matthieu Sozeau	2016-06-16
*	Implement limited proof search and iterative deepening.	Matthieu Sozeau	2016-06-16
*	Typeclasses eauto based on new proof engine,	Matthieu Sozeau	2016-06-16
*	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
*	Moving Eauto and Class_tactics to tactics/.	Pierre-Marie Pédrot	2016-03-25
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Update headers.	Maxime Dénès	2015-01-12
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	Splitting Class_tactics between code and CAMLP4/5 declarations.	ppedrot	2013-10-04