coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-11-21	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias
	We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-09-08	Unplugging Pptactic from Ppvernac.	Pierre-Marie Pédrot

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

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

2012-10-04	Moved Compat to parsing. This permits to break the dependency of the	ppedrot
	kernel on CAMLP4/5 structures, and consequently should also erase such structures from vo files. This modification requires some code duplication, mainly while reimplementing our own location data type. This is chiefly visible in the ml4 files, where CAMLP4/5 locations must be manually converted to our locations with an explicit (!@) cast operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7