aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/tok.mli
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | longer use camlp4.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Revert "Move bullet detection from lexer to parser (bug #5102)."Gravatar Guillaume Melquiond2016-10-05
| | | | This reverts commit 466b7e69e49a5f4bba36b834a2e046f120ece07c.
* Move bullet detection from lexer to parser (bug #5102).Gravatar Guillaume Melquiond2016-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.Gravatar Maxime Dénès2016-07-03
| | | | | This was implemented in anticipation of a part of PR#164 that we decided not to merge.
* Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Gravatar Pierre-Marie Pédrot2016-03-06
| | | | | | | | We just reuse the same one weird old trick in CAMLP4 to compare keywords and identifiers as tokens. Note though that the commit 982460743 does not fix the keyword vs. identifier issue in CAMLP4, so that the corresponding test fails. This means that since that commit, some code compiling with CAMLP5 does not when using CAMLP4, making it a second-class citizen.
* Removing the METAIDENT token, as it is not used anymore.Gravatar Pierre-Marie Pédrot2016-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'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Adding a token "index" representing positions (1st, 2nd, etc.).Gravatar Hugo Herbelin2015-12-15
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
|
* Revert "KEYID token makes parsing more robust in face of notations"Gravatar gareuselesinge2013-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 notationsGravatar gareuselesinge2013-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.Gravatar herbelin2012-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 Camlp4Gravatar pboutill2012-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 mechanismGravatar pboutill2012-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 trunkGravatar herbelin2010-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.Gravatar herbelin2010-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*Gravatar letouzey2010-05-19
Cf tok.ml, token isn't anymore string*string where first string encodes the kind of the token, but rather a nice sum type. Unfortunately, string*string (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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-11 15:24:32 +0000