coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixing Camlp4 compilation.	ppedrot	2013-06-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16613 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
\| \| \| \| \| \|	mechanism to retrieve the same information. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Avoiding collision between Camlp4 Loc.Exc_located and Coq's Loc.Exc_located.	herbelin	2012-12-22
\| \| \| \| \| \| \|	Also fixing coqmktop for use with Camlp4. Don't know if this is the fix intended by coqmktop experts or not, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Early translation of camlp4/camlp5 located errors into coq-located	herbelin	2012-12-04
\| \| \| \| \| \| \| \|	errors so as to be able to work only with Loc.Exc_located inside main Coq. This fixes the anomaly (probably introduced by commit 15847) when a syntax error arrives in coqc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	restore compatibility with camlp5 < 6.00	letouzey	2012-10-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15881 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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