diff options
-rw-r--r-- | grammar/q_util.ml4 | 16 | ||||
-rw-r--r-- | grammar/q_util.mli | 16 |
2 files changed, 16 insertions, 16 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 682188732..53e1f008d 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -17,14 +17,14 @@ type argument_type = | ExtraArgType of string type user_symbol = -| Ulist1 : user_symbol -> user_symbol -| Ulist1sep : user_symbol * string -> user_symbol -| Ulist0 : user_symbol -> user_symbol -| Ulist0sep : user_symbol * string -> user_symbol -| Uopt : user_symbol -> user_symbol -| Umodifiers : user_symbol -> user_symbol -| Uentry : string -> user_symbol -| Uentryl : string * int -> user_symbol +| Ulist1 of user_symbol +| Ulist1sep of user_symbol * string +| Ulist0 of user_symbol +| Ulist0sep of user_symbol * string +| Uopt of user_symbol +| Umodifiers of user_symbol +| Uentry of string +| Uentryl of string * int type extend_token = | ExtTerminal of string diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 7d4cc0200..8c437b42a 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -15,14 +15,14 @@ type argument_type = | ExtraArgType of string type user_symbol = -| Ulist1 : user_symbol -> user_symbol -| Ulist1sep : user_symbol * string -> user_symbol -| Ulist0 : user_symbol -> user_symbol -| Ulist0sep : user_symbol * string -> user_symbol -| Uopt : user_symbol -> user_symbol -| Umodifiers : user_symbol -> user_symbol -| Uentry : string -> user_symbol -| Uentryl : string * int -> user_symbol +| Ulist1 of user_symbol +| Ulist1sep of user_symbol * string +| Ulist0 of user_symbol +| Ulist0sep of user_symbol * string +| Uopt of user_symbol +| Umodifiers of user_symbol +| Uentry of string +| Uentryl of string * int type extend_token = | ExtTerminal of string |