coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias	2017-10-10
\| \| \| \| \| \| \| \| \|	We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	[pp] Remove unused printing tagging infrastructure.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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.
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Plug the dynamic tags in the Richpp mechanism.	Pierre-Marie Pédrot	2014-11-10
\|
*	lib/RichPp: Rename into Richpp.	Yann Régis-Gianas	2014-11-05
\| \| \| \| \| \|	printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics.
*	Ppvernac: Publish new rich pretty-printer.	Regis-Gianas	2014-11-04
\| \| \| \|	Ppconstr: Fix a typo in comments.
*	Ppvernacsig: New.	Regis-Gianas	2014-11-04
\| \| \| \| \| \|	- Define the signature for a pretty-printer of vernacular commands. Ppvernac: Use it.
*	A few fixes to the build system (mostly for ocamlbuild)	Pierre Letouzey	2013-12-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	* vars.mli was mentionning Term instead of Constr, leading to a dep cycle * Having a file named toplevel/toplevel.ml isn't a good idea when we also have a toplevel/toplevel.mllib that ought to produce a toplevel.cma. We rename toplevel.ml into Coqloop.ml * Extra cleanup of toplevel.mllib : - Ppextra isn't anywhere around (?!) - Ppvernac was mentionned twice, and rather belongs to printing.mllib anyway - Vernacexpr is a .mli and shouldn't appear in an .mllib * During the link, printing.cma now comes after parsing.cma (Ppvernac uses Egramml) * A few extra -threads in ocamlbuild files (btw, it's a bit sad to need -thread for coqchk).
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixes a bug in Ppvernac which had braces and bullets printed with an ending	aspiwack	2012-07-04
\| \| \| \| \| \|	period. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15509 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
*	place all pretty-printing files in new dir printing/	letouzey	2012-05-29
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7