coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Post-rebase warnings (unused opens and 2 unused values)	Gaetan Gilbert	2017-04-27
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Removing various tactic compatibility layers in core tactics.	Pierre-Marie Pédrot	2017-04-24
*	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\
* \|	Removing most nf_enter in tactics.	Pierre-Marie Pédrot	2017-02-14
* \|	Class_tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	Hints API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| *	Rework search_strategy option handling	Matthieu Sozeau	2016-11-03
\| *	Internal API change to typeclasses eauto.	Théo Zimmermann	2016-11-03
\| *	Fix handling of only_classes at toplevel	Matthieu Sozeau	2016-11-03
\| *	Fix Typeclasses eauto := bfs.	Matthieu Sozeau	2016-11-03
\|/
*	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