coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-18
\|\
\| *	[toplevel] Remove duplicate beautify flags.	Emilio Jesus Gallego Arias	2016-10-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Given the current style in flags.mli no reason to have a function. A deeper question is why a global flag is needed, in particular the use in `interp/constrextern.ml` seems strange, the condition in the lexer should be looked at and I'm not sure about `printing/`.
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\|
\| *	Moving Pp.comments to CLexer so that Pp is purer (no more side-effect	Hugo Herbelin	2016-10-09
\| \| \| \| \| \| \| \| \| \|	done by the Ppcmd_comment token) and so that lexing/parsing side-effects are collected at the same place, i.e. in CLexer.
* \|	Unplugging Pptactic from Ppvernac.	Pierre-Marie Pédrot	2016-09-08
\|/
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
	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