Removing a source of type-unsafeness in Pcoq.

2 files changed, 9 insertions, 12 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index e9c3a7073d..465073b7aa 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -387,16 +387,16 @@ let create_ltac_quotation name cast wit e =
   let () = ltac_quotations := String.Set.add name !ltac_quotations in
 (*   let level = Some "1" in *)
   let level = None in
-  let assoc = Some (of_coq_assoc Extend.RightA) in
-  let rule = [
-    gram_token_of_string name;
-    gram_token_of_string ":";
-    symbol_of_prod_entry_key (Aentry (name_of_entry e));
-  ] in
+  let assoc = Some Extend.RightA in
+  let rule =
+    Next (Next (Next (Stop,
+      Atoken (Lexer.terminal name)),
+      Atoken (Lexer.terminal ":")),
+      Aentry (name_of_entry e))
+  in
   let action v _ _ loc =
-    let loc = !@loc in
     let arg = TacGeneric (Genarg.in_gen (Genarg.rawwit wit) (cast (loc, v))) in
     TacArg (loc, arg)
   in
-  let gram = (level, assoc, [rule, Gram.action action]) in
-  maybe_uncurry (Gram.extend Tactic.tactic_expr) (None, [gram])
+  let gram = (level, assoc, [Rule (rule, action)]) in
+  Pcoq.grammar_extend Tactic.tactic_expr None (None, [gram])
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 9b3a96975f..b26c3044bd 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -274,9 +274,6 @@ val name_of_entry : 'a Gram.entry -> 'a Entry.t
 
 (** Binding general entry keys to symbols *)
 
-val symbol_of_prod_entry_key :
-  ('self, 'a) entry_key -> Gram.symbol
-
 type 's entry_name = EntryName :
   'a raw_abstract_argument_type * ('s, 'a) entry_key -> 's entry_name