coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-04-11	Removing the ad-hoc tactic_expr type.	Pierre-Marie Pédrot
	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.
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.