diff options
Diffstat (limited to 'grammar/q_util.ml4')
| -rw-r--r-- | grammar/q_util.ml4 | 16 |
1 files changed, 8 insertions, 8 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 |