Getting rid of the Atactic entry.

3 files changed, 18 insertions, 14 deletions

diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 5b005186b..20c83dfaf 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -58,6 +58,6 @@ let rec mlexpr_of_prod_entry_key : type s a. (s, a) Pcoq.entry_key -> _ = functi
   | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >>
   | Pcoq.Aself -> <:expr< Pcoq.Aself >>
   | Pcoq.Anext -> <:expr< Pcoq.Anext >>
-  | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >>
   | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:s$) >>
-  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >>
+  | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry ($str:u$, $str:s$) >>
+  | Pcoq.Aentryl ((u,s), l) -> <:expr< Pcoq.Aentryl ($str:u$, $str:s$) $mlexpr_of_int l$ >>
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index b1692e9e2..b244a021e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -76,8 +76,8 @@ type ('self, _) entry_key =
 | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
 | Aself : ('self, 'self) entry_key
 | Anext : ('self, 'self) entry_key
-| Atactic : int -> ('self, Tacexpr.raw_tactic_expr) entry_key
 | Aentry : (string * string) -> ('self, 'a) entry_key
+| Aentryl : (string * string) * int -> ('self, 'a) entry_key
 
 type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name
 
@@ -370,8 +370,8 @@ module Tactic =
 
     (* Main entries for ltac *)
     let tactic_arg = Gram.entry_create "tactic:tactic_arg"
-    let tactic_expr = Gram.entry_create "tactic:tactic_expr"
-    let binder_tactic = Gram.entry_create "tactic:binder_tactic"
+    let tactic_expr = make_gen_entry utactic (rawwit wit_tactic)  "tactic_expr"
+    let binder_tactic = make_gen_entry utactic (rawwit wit_tactic) "binder_tactic"
 
     let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic"
 
@@ -707,12 +707,12 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function
 	   Gram.action (fun _ l _ _loc -> l))]
   | Aself -> Symbols.sself
   | Anext -> Symbols.snext
-  | Atactic 5 -> Symbols.snterm (Gram.Entry.obj Tactic.binder_tactic)
-  | Atactic n ->
-      Symbols.snterml (Gram.Entry.obj Tactic.tactic_expr, string_of_int n)
   | Aentry (u,s) ->
     let e = get_entry (get_univ u) s in
     Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e))
+  | Aentryl ((u, s), n) ->
+    let e = get_entry (get_univ u) s in
+    Symbols.snterml (Gram.Entry.obj (object_of_typed_entry e), string_of_int n)
 
 let level_of_snterml e = int_of_string (Symbols.snterml_level e)
 
@@ -740,6 +740,14 @@ let tactic_level s =
 let type_of_entry u s =
   type_of_typed_entry (get_entry u s)
 
+let name_of_entry e = match String.split ':' (Gram.Entry.name e) with
+| u :: s :: [] -> (u, s)
+| _ -> assert false
+
+let atactic n =
+  if n = 5 then Aentry (name_of_entry Tactic.binder_tactic)
+  else Aentryl (name_of_entry Tactic.tactic_expr, n)
+
 let rec interp_entry_name static up_level s sep =
   let l = String.length s in
   if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then
@@ -777,7 +785,7 @@ let rec interp_entry_name static up_level s sep =
         let se =
           if check_lvl n then Aself
           else if check_lvl (n + 1) then Anext
-          else Atactic n
+          else atactic n
         in
         (Some t, se)
       | None ->
@@ -794,10 +802,6 @@ 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 d13ff548c..959c039d3 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -273,8 +273,8 @@ type ('self, _) entry_key =
 | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key
 | Aself : ('self, 'self) entry_key
 | Anext : ('self, 'self) entry_key
-| Atactic : int -> ('self, raw_tactic_expr) entry_key
 | Aentry : (string * string) -> ('self, 'a) entry_key
+| Aentryl : (string * string) * int -> ('self, 'a) entry_key
 
 val name_of_entry : 'a Gram.entry -> string * string