coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-03-21	[pp] Remove unused printing tagging infrastructure.	Emilio Jesus Gallego Arias
	Applications of it were not clear/unproven, it made printers more complex (as they needed to be functors) and as it lacked examples it confused some people. The printers now tag unconditionally, it is up to the backends to interpreted the tags. Tagging (and indeed the notion of rich document) should be reworked in a follow-up patch, so they are in sync, but this is a first step. Tested, test-suite passes. Notes: - We remove the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in sync). - Note that Richpp didn't need a single change. In particular, its main API entry point `Richpp.rich_pp` is not used by anyone.
2016-09-29	Fix bug #4869, allow Prop, Set, and level names in constraints.	Matthieu Sozeau

2016-06-16	Fixing printing of Instance.	Hugo Herbelin

2016-04-27	Revert "Fixing printing of Instance."	Hugo Herbelin
	This reverts commit cbb917476e3920641352c108ec9ffaf6d1682217.
2016-04-27	Fixing printing of Instance.	Hugo Herbelin

2016-01-20	Update copyright headers.	Maxime Dénès

2015-02-02	Removing dead code.	Pierre-Marie Pédrot

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

2014-11-17	Moving printing code for red_expr and may_eval to Pptactic.	Pierre-Marie Pédrot

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.