coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
	Now it is a private field, locations are optional.
2017-03-24	Renaming local_binder into local_binder_expr.	Hugo Herbelin
	This is a bit long, but it is to keep a symmetry with constr_expr.
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-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-05	lib/RichPp: Rename into Richpp.	Yann Régis-Gianas
	printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics.
2014-11-04	Ppvernac: Publish new rich pretty-printer.	Regis-Gianas
	Ppconstr: Fix a typo in comments.
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.
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
	With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2012-12-18	Modulification of name	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14	Modulification of identifier	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
	were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-19	Fixing some inconsistencies of constr printer wrt constr parser	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15447 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	place all pretty-printing files in new dir printing/	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7