diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-15 18:26:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-24 19:16:33 +0200 |
| commit | b090942f20ac8854bf227698d31ca1efec492c47 (patch) | |
| tree | 61cdc57146c4151fa743de9b3c2ab59b11722f92 /intf | |
| parent | f3515efc26a693f4c525ad91c37c982f4c96e6ec (diff) | |
Higher-level API for tactic notations.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/extend.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/intf/extend.mli b/intf/extend.mli index 10713745e..381d47dd1 100644 --- a/intf/extend.mli +++ b/intf/extend.mli @@ -53,14 +53,14 @@ type simple_constr_prod_entry_key = (** {5 AST for user-provided entries} *) -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 -| Uentry : string -> user_symbol -| Uentryl : string * int -> user_symbol +type 'a user_symbol = +| Ulist1 of 'a user_symbol +| Ulist1sep of 'a user_symbol * string +| Ulist0 of 'a user_symbol +| Ulist0sep of 'a user_symbol * string +| Uopt of 'a user_symbol +| Uentry of 'a +| Uentryl of 'a * int (** {5 Type-safe grammar extension} *) |