diff options
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 26 |
1 files changed, 15 insertions, 11 deletions
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 |