coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix incorrect token description for bullets.	Guillaume Melquiond	2016-10-05
\|
*	Revert "Move bullet detection from lexer to parser (bug #5102)."	Guillaume Melquiond	2016-10-05
\| \| \| \|	This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.
*	Move bullet detection from lexer to parser (bug #5102).	Guillaume Melquiond	2016-10-02
\| \| \| \| \| \| \| \| \| \|	That way, bullet detection no longer depends on a global variable indicating whether a line is starting. This causes a small change in the recognized language. Before the commit, "--++" was recognized as a bullet "--" followed by a keyword "++" when at the start of a line; now it is always recognized as a keyword "--++". This also fixes a bug in Tok.to_string as a side-effect.
*	Remove lexing of ordinal notations.	Maxime Dénès	2016-07-03
\| \| \| \| \|	This was implemented in anticipation of a part of PR#164 that we decided not to merge.
*	Further reducing the dependencies of the EXTEND macros.	Pierre-Marie Pédrot	2016-03-19
\|
*	Removing the METAIDENT token, as it is not used anymore.	Pierre-Marie Pédrot	2016-02-24
\| \| \| \| \| \|	METAIDENT were idents of the form $foobar, only used in quotations. Note that it removes two dollars in the Coq codebase! Guess I'm absolved for the $(...) syntax.
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Adding a token "index" representing positions (1st, 2nd, etc.).	Hugo Herbelin	2015-12-15
\|/
*	Fixing the "parsing rules with idents later declared as keywords" problem.	Hugo Herbelin	2015-11-26
\| \| \| \| \| \| \|	The fix was actually elementary. The lexer comes with a function to compare parsed tokens against tokens of the parsing rules. It is enough to have this function considering an ident in a parsing rule to be equal to the corresponding string parsed as a keyword.
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Uncountably many bullets (+,-,,++,--,*,+++,...).	Hugo Herbelin	2014-08-05
\|
*	Removing some generic equalities.	ppedrot	2013-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Revert "KEYID token makes parsing more robust in face of notations"	gareuselesinge	2013-06-21
\| \| \| \| \| \|	This reverts commit 950086cd26f83aa8896dde9dc7ef5b3d87307c56. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16599 85f007b7-540e-0410-9357-904b9bb8a0f7
*	KEYID token makes parsing more robust in face of notations	gareuselesinge	2013-06-19
\| \| \| \| \| \| \| \| \|	A notation may introduce a new keyword that masks an quasi keyword (IDENT "of" for example) used in some grammar rules. KEYID "of" acepts both "of" as an ident and "of" as a keyword. Rephrasing grammar rules with KEYID makes hence them more robust in face of user notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16590 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Partial revert of r15148 in order to compile with Camlp4	pboutill	2012-04-27
\| \| \| \| \| \|	+ comment correction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15253 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove print call that do not use the pp mechanism	pboutill	2012-04-12
\| \| \| \| \| \|	Signed-off-by: Edward Z. Yang <ezyang@mit.edu> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
\| \| \| \| \| \|	Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nicer representation of tokens, more independant of camlp*	letouzey	2010-05-19
	Cf tok.ml, token isn't anymore stringstring where first string encodes the kind of the token, but rather a nice sum type. Unfortunately, stringstring (a.k.a Plexing.pattern) is still used in some places of Camlp5, so there's a few conversions back and forth. But the penalty should be quite low, and having nicer tokens helps in the forthcoming integration of support for camlp4 post 3.10 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13018 85f007b7-540e-0410-9357-904b9bb8a0f7