diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | ltac/tacentries.ml | 23 |
2 files changed, 11 insertions, 14 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..5720a6f378 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 @@ -139,17 +139,17 @@ let rec prod_item_of_symbol lev = function EntryName (Rawwit (ListArg typ), Alist0 e) | Extend.Ulist1sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1sep (e, sep)) + EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep))) | Extend.Ulist0sep (s, sep) -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0sep (e, sep)) + EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep))) | Extend.Uopt s -> let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in EntryName (Rawwit (OptArg typ), Aopt e) | 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); @@ -157,7 +157,7 @@ let rec prod_item_of_symbol lev = function (** Tactic grammar extensions *) -let add_tactic_entry (kn, ml, tg) = +let add_tactic_entry (kn, ml, tg) state = let open Tacexpr in let entry, pos = get_tactic_entry tg.tacgram_level in let mkact loc l = @@ -184,14 +184,13 @@ let add_tactic_entry (kn, ml, tg) = in let prods = List.map map tg.tacgram_prods in let rules = make_rule mkact prods in - synchronize_level_positions (); - grammar_extend entry None (pos, [(None, None, List.rev [rules])]); - 1 + let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in + ([r], state) let tactic_grammar = create_grammar_command "TacticGrammar" add_tactic_entry -let extend_tactic_grammar kn ml ntn = extend_grammar tactic_grammar (kn, ml, ntn) +let extend_tactic_grammar kn ml ntn = extend_grammar_command tactic_grammar (kn, ml, ntn) (**********************************************************************) (* Tactic Notation *) @@ -389,8 +388,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 |