coq - The formal proof system

Age	Commit message (Collapse)	Author
2016-09-21	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot
	There was no reason to keep them separate since quite a long time. Historically, they were making Genarg depend or not on upper strata of the code, but since it was moved to lib/ this is not justified anymore.
2016-09-15	Made Ppanotation Ltac-agnostic.	Pierre-Marie Pédrot

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.