From f832476404a29d7791c1a6d7970988d3b2e3ad9e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 18 Mar 2019 15:17:55 +0100
Subject: documentation

---
 gramlib/plexing.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'gramlib')

diff --git a/gramlib/plexing.mli b/gramlib/plexing.mli
index 48722e01be..26443df026 100644
--- a/gramlib/plexing.mli
+++ b/gramlib/plexing.mli
@@ -14,7 +14,7 @@ type pattern = string * string option
 -      The first string is the constructor name (must start with
        an uppercase character). When it is empty, the second string
        is supposed to be a keyword.
--      The second string is the constructor parameter. Empty if it
+-      The second component is the constructor parameter. None if it
        has no parameter (corresponding to the 'wildcard' pattern).
 -      The way tokens patterns are interpreted to parse tokens is done
        by the lexer, function [tok_match] below. *)
-- 
cgit v1.2.3