From b090942f20ac8854bf227698d31ca1efec492c47 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 15 Apr 2016 18:26:28 +0200 Subject: Higher-level API for tactic notations. --- intf/extend.mli | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'intf') 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} *) -- cgit v1.2.3