diff options
| author | Pierre-Marie Pédrot | 2016-03-19 20:42:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-19 20:42:51 +0100 |
| commit | 25d49062425ee080d3e8d06920d3073e7a81b603 (patch) | |
| tree | 95cf1b3dafb43b6c9912b4d630e96078b12b04a3 | |
| parent | 13dd3f8ebaf90f30afbcb48034e5bdd90c825765 (diff) | |
Fixing compilation with old versions of CAMLP5.
| -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 6821887327..53e1f008d9 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 7d4cc0200a..8c437b42a1 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 |