Supporting locality flag for custom entries + compatibility with modules.

Also prevents to use an entry name already defined.

1 files changed, 4 insertions, 3 deletions

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9711cd0461..b2e1259646 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -273,7 +273,8 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry
 val register_grammars_by_name : string -> any_entry list -> unit
 val find_grammars_by_name : string -> any_entry list
 
-(** Create a custom entry of some name *)
+(** Create a custom entry of some name; boolean is [true] if local *)
 
-val create_custom_entries : string -> unit
-val find_custom_entries : string -> (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)
+val create_custom_entry : bool -> string -> unit
+val find_custom_entry : string -> (Constrexpr.constr_expr Gram.entry * Constrexpr.cases_pattern_expr Gram.entry)
+val locality_of_custom_entry : string -> bool