Getting rid of the Agram entry.

4 files changed, 10 insertions, 21 deletions

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index b1eabdd98b..5b005186bd 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -59,6 +59,5 @@ let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = functi
   | Pcoq.Aself -> <:expr< Pcoq.Aself >>
   | Pcoq.Anext -> <:expr< Pcoq.Anext >>
   | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >>
-  | Pcoq.Agram s -> Errors.anomaly (Pp.str "Agram not supported")
-  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.name $lid:s$) >>
+  | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >>
   | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index d9eb5d4126..fba754eaaf 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -378,7 +378,7 @@ let create_ltac_quotation name cast wit e =
   let rule = [
     gram_token_of_string name;
     gram_token_of_string ":";
-    symbol_of_prod_entry_key (Agram (Gram.Entry.name e));
+    symbol_of_prod_entry_key (Aentry (name_of_entry e));
   ] in
   let action v _ _ loc =
     let loc = !@loc in
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 63662a9561..b1692e9e2b 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -77,8 +77,7 @@ type ('self, _) entry_key =
 | Aself : ('self, 'self) entry_key
 | Anext : ('self, 'self) entry_key
 | Atactic : int -> ('self, Tacexpr.raw_tactic_expr) entry_key
-| Agram : string -> ('self, 'a) entry_key
-| Aentry : string * string -> ('self, 'a) entry_key
+| Aentry : (string * string) -> ('self, 'a) entry_key
 
 type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name
 
@@ -711,20 +710,6 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
   | Atactic 5 -> Symbols.snterm (Gram.Entry.obj Tactic.binder_tactic)
   | Atactic n ->
       Symbols.snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
-  | Agram s ->
-    let e =
-      try
-      (** ppedrot: we should always generate Agram entries which have already
-          been registered, so this should not fail. *)
-        let (u, s) = match String.split ':' s with
-        | u :: s :: [] -> (u, s)
-        | _ -> raise Not_found
-        in
-        get_entry (get_univ u) s
-      with Not_found ->
-        Errors.anomaly (str "Unregistered grammar entry: " ++ str s)
-    in
-    Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e))
   | Aentry (u,s) ->
     let e = get_entry (get_univ u) s in
     Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e))
@@ -809,6 +794,10 @@ let rec interp_entry_name static up_level s sep =
 	| None -> ExtraArgType s in
     EntryName (t, se)
 
+let name_of_entry e = match String.split ':' (Gram.Entry.name e) with
+| u :: s :: [] -> (u, s)
+| _ -> assert false
+
 let list_entry_names () =
   let add_entry key (entry, _) accu = (key, entry) :: accu in
   let ans = Hashtbl.fold add_entry (snd uprim) [] in
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index cdffbcba50..d13ff548ca 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -274,8 +274,9 @@ type ('self, _) entry_key =
 | Aself : ('self, 'self) entry_key
 | Anext : ('self, 'self) entry_key
 | Atactic : int -> ('self, raw_tactic_expr) entry_key
-| Agram : string -> ('self, 'a) entry_key
-| Aentry : string * string -> ('self, 'a) entry_key
+| Aentry : (string * string) -> ('self, 'a) entry_key
+
+val name_of_entry : 'a Gram.entry -> string * string
 
 (** Binding general entry keys to symbols *)