coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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.