coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant.
*	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
\|/ \| \| \| \|	Furthermore, ML tactic dispatch is not done according to the type of its argument anymore.
*	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/Pptactic: Tag tactics pretty-printing. printing/Ppvernac: Use the relevent Pptactic pretty-printer. printing/RichPrinter: Publish two new services.
*	printing/Pptacticsig: New signature for tactic pretty-printers.	Regis-Gianas	2014-11-04
	printing/Pptactic: Use it.