coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert "Passing around the precedence to the generic printer so as to solve"	Hugo Herbelin	2016-04-27
*	Passing around the precedence to the generic printer so as to solve	Hugo Herbelin	2016-04-27
*	Removing the ad-hoc tactic_expr type.	Pierre-Marie Pédrot	2016-04-11
*	Fixing printing of toplevel values.	Pierre-Marie Pédrot	2016-04-08
*	Moving Tactic_debug to tactics/ folder.	Pierre-Marie Pédrot	2016-03-06
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Reduce dependencies of interface files.	Guillaume Melquiond	2016-01-02
* \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \|	Using dynamic values in tactic evaluation.	Pierre-Marie Pédrot	2015-12-21
* \|	Tying the loop in tactic printing API.	Pierre-Marie Pédrot	2015-12-18
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-10
\|\\|
\| *	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
* \|	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot	2015-01-23
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Moving printing code for red_expr and may_eval to Pptactic.	Pierre-Marie Pédrot	2014-11-17
*	printing/Ppannotation: New annotation for tactic syntactic objects.	Regis-Gianas	2014-11-04
*	printing/Pptacticsig: New signature for tactic pretty-printers.	Regis-Gianas	2014-11-04