diff options
Diffstat (limited to 'gramlib/plexing.mli')
| -rw-r--r-- | gramlib/plexing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli index f6e4d96b80..48722e01be 100644 --- a/gramlib/plexing.mli +++ b/gramlib/plexing.mli @@ -8,7 +8,7 @@ grammars (see module [Grammar]). It also provides some useful functions to create lexers. *) -type pattern = string * string +type pattern = string * string option (* Type for values used by the generated code of the EXTEND statement to represent terminals in entry rules. - The first string is the constructor name (must start with |