Removing the Entry module now that rules need not be marshalled.

2 files changed, 5 insertions, 7 deletions

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 1bbdb17790..0c25481d8e 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -43,8 +43,6 @@ let tactic_mode = Gram.entry_create "vernac:tactic_command"
 
 let new_entry name =
   let e = Gram.entry_create name in
-  let entry = Entry.create name in
-  let () = Pcoq.set_grammar entry e in
   e
 
 let selector = new_entry "vernac:selector"
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml
index 881482081a..d0383ffbcb 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -43,8 +43,8 @@ let coincide s pat off =
   !break
 
 let atactic n =
-  if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
-  else Aentryl (name_of_entry Tactic.tactic_expr, n)
+  if n = 5 then Aentry Tactic.binder_tactic
+  else Aentryl (Tactic.tactic_expr, n)
 
 type entry_name = EntryName :
   'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name
@@ -149,7 +149,7 @@ let rec prod_item_of_symbol lev = function
 | Extend.Uentry arg ->
   let ArgT.Any tag = arg in
   let wit = ExtraArg tag in
-  EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit)))
+  EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit))
 | Extend.Uentryl (s, n) ->
   let ArgT.Any tag = s in
   assert (coincide (ArgT.repr tag) "tactic" 0);
@@ -389,8 +389,8 @@ let create_ltac_quotation name cast (e, l) =
   in
   let () = ltac_quotations := String.Set.add name !ltac_quotations in
   let entry = match l with
-  | None -> Aentry (name_of_entry e)
-  | Some l -> Aentryl (name_of_entry e, l)
+  | None -> Aentry e
+  | Some l -> Aentryl (e, l)
   in
 (*   let level = Some "1" in *)
   let level = None in