coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Removing the ad-hoc tactic_expr type.	Pierre-Marie Pédrot	2016-04-11
\| \| \| \| \| \| \| \| \| \|	This type was actually only used by the debug printer of tactics, and only for atomic tactics. Furthermore, that type was asymmetric, as the underlying tacexpr type was set to be glob_tactic, when the semantics would have required a Val.t type. Furthermore, this type is absent from every contrib I have seen, which hints again in favour of its lack of meaning.
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Plug the dynamic tags in the Richpp mechanism.	Pierre-Marie Pédrot	2014-11-10
\|
*	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/Ppannotation: Introduce a new annotation for keywords.	Regis-Gianas	2014-11-04
\| \| \| \|	printing/{Ppconstr, Ppvernac}: Use it.
*	printing/RichPrinter: New API for rich pretty-printing.	Regis-Gianas	2014-11-04
\| \| \| \| \|	printing/Ppannotation: Define the projection of annotations into XML attributes. lib/richPp: Implements valid entities escaping.
*	Ppannotation.t: New constructor AVernac.	Regis-Gianas	2014-11-04
\| \| \| \|	Ppvernac.RichPp: New rich pretty-printer.
*	Ppannotation: New.	Regis-Gianas	2014-11-04
	Define the annotations stored in semi-structured pretty-prints. Ppconstrsig: New. Contains the signature of a pretty-printer for ppconstr. Ppconstr: Export a new rich pretty-printer for constr_expr and co.