coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-11-10	Plug the dynamic tags in the Richpp mechanism.	Pierre-Marie Pédrot

2014-11-04	printing/Ppannotation: New annotation for tactic syntactic objects.	Regis-Gianas
	printing/Pptactic: Tag tactics pretty-printing. printing/Ppvernac: Use the relevent Pptactic pretty-printer. printing/RichPrinter: Publish two new services.
2014-11-04	printing/Ppannotation: Introduce a new annotation for keywords.	Regis-Gianas
	printing/{Ppconstr, Ppvernac}: Use it.
2014-11-04	printing/RichPrinter: New API for rich pretty-printing.	Regis-Gianas
	printing/Ppannotation: Define the projection of annotations into XML attributes. lib/richPp: Implements valid entities escaping.
2014-11-04	Ppannotation.t: New constructor AVernac.	Regis-Gianas
	Ppvernac.RichPp: New rich pretty-printer.
2014-11-04	Ppannotation: New.	Regis-Gianas
	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.