coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
\| \| \| \| \|	As noticed by C. Cohen it was confusingly different from standard notation.
*	Typeclasses eauto based on new proof engine,	Matthieu Sozeau	2016-06-16
\| \| \| \|	with full backtracking across multiple goals.
*	Revert "Fixing printers for pr_auto_using and pr_firstorder_using."	Hugo Herbelin	2016-04-27
\| \| \| \|	This reverts commit 23ebfc41fba48ccce9bc878de258d1b0901f7dda.
*	Fixing printers for pr_auto_using and pr_firstorder_using.	Hugo Herbelin	2016-04-27
\|
*	Removing redundant *_TYPED AS clauses in EXTEND statements.	Pierre-Marie Pédrot	2016-04-12
\|
*	Moving type_uconstr to Pretyping.	Pierre-Marie Pédrot	2016-03-25
\|
*	Creating a dedicated ltac/ folder for Hightactics.	Pierre-Marie Pédrot	2016-03-21