From 8a3b19b62720e2324ef24003407c2e83335a51a5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 16 Jan 2016 14:57:48 +0100
Subject: Separating the parsing of user-defined entries from their
 intepretation.

---
 intf/extend.mli | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'intf')

diff --git a/intf/extend.mli b/intf/extend.mli
index 975f194b07..651fa638b5 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -51,6 +51,18 @@ type constr_prod_entry_key =
 type simple_constr_prod_entry_key =
     (production_level,unit) constr_entry_key_gen
 
+(** {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
+| Umodifiers : user_symbol -> user_symbol
+| Uentry : string -> user_symbol
+| Uentryl : string * int -> user_symbol
+
 (** {5 Type-safe grammar extension} *)
 
 type ('self, 'a) symbol =
-- 
cgit v1.2.3