diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/extend.ml | 6 | ||||
| -rw-r--r-- | parsing/tok.mli | 1 |
2 files changed, 4 insertions, 3 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index 050ed49622..9b5537d7f6 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -106,11 +106,11 @@ type 'a production_rule = type 'a single_extend_statement = string option * - (** Level *) + (* Level *) Gramlib.Gramext.g_assoc option * - (** Associativity *) + (* Associativity *) 'a production_rule list - (** Symbol list with the interpretation function *) + (* Symbol list with the interpretation function *) type 'a extend_statement = Gramlib.Gramext.position option * diff --git a/parsing/tok.mli b/parsing/tok.mli index 9b8c008555..55fcd33272 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -27,6 +27,7 @@ val to_string : t -> string (* Needed to fit Camlp5 signature *) val print : Format.formatter -> t -> unit val match_keyword : string -> t -> bool + (** for camlp5 *) val of_pattern : string*string -> t val to_pattern : t -> string*string |