Store marshallable data in the custom entry summary.

3 files changed, 31 insertions, 2 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 720f9b774a..16101396cf 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -250,6 +250,32 @@ type (_, _) entry =
 
 type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry
 
+let constr_custom_entry : (string, Constrexpr.constr_expr) entry_command =
+  create_entry_command "constr" (fun s st -> [s], st)
+let pattern_custom_entry : (string, Constrexpr.cases_pattern_expr) entry_command =
+  create_entry_command "pattern" (fun s st -> [s], st)
+
+let custom_entry_locality = Summary.ref ~name:"LOCAL-CUSTOM-ENTRY" String.Set.empty
+(** If the entry is present then local *)
+
+let create_custom_entry ~local s =
+  if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then
+    user_err Pp.(quote (str s) ++ str " is a reserved entry name.");
+  let sc = "constr:"^s in
+  let sp = "pattern:"^s in
+  let _ = extend_entry_command constr_custom_entry sc in
+  let _ = extend_entry_command pattern_custom_entry sp in
+  let () = if local then custom_entry_locality := String.Set.add s !custom_entry_locality in
+  ()
+
+let find_custom_entry s =
+  let sc = "constr:"^s in
+  let sp = "pattern:"^s in
+  try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
+  with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
+
+let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality
+
 (* This computes the name of the level where to add a new rule *)
 let interp_constr_entry_key : type r. _ -> r target -> int -> r Entry.t * int option =
   fun custom forpat level ->
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index b0341e6a17..3a6f8ae015 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -17,3 +17,6 @@
 
 val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
+
+val create_custom_entry : local:bool -> string -> unit
+val locality_of_custom_entry : string -> bool
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 34e18938dc..d66a121437 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1218,7 +1218,7 @@ let check_locality_compatibility local custom i_typs =
     let subcustom = List.map_filter (function _,ETConstr (InCustomEntry s,_,_) -> Some s | _ -> None) i_typs in
     let allcustoms = match custom with InCustomEntry s -> s::subcustom | _ -> subcustom in
     List.iter (fun s ->
-        if Pcoq.locality_of_custom_entry s then
+        if Egramcoq.locality_of_custom_entry s then
           user_err (strbrk "Notation has to be declared local as it depends on custom entry " ++ str s ++
                     strbrk " which is local."))
       (List.uniquize allcustoms)
@@ -1645,7 +1645,7 @@ let add_syntactic_definition env ident (vars,c) local onlyparse =
 let load_custom_entry _ _ = ()
 
 let open_custom_entry _ (_,(local,s)) =
-  Pcoq.create_custom_entry local s
+  Egramcoq.create_custom_entry ~local s
 
 let cache_custom_entry o =
   load_custom_entry 1 o;