diff options
Diffstat (limited to 'ltac/tacentries.ml')
| -rw-r--r-- | ltac/tacentries.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index d05beb392..fcdb1875d 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 Tactic.binder_tactic - else Aentryl (Tactic.tactic_expr, n) + if n = 5 then Aentry Pltac.binder_tactic + else Aentryl (Pltac.tactic_expr, n) type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name @@ -108,11 +108,11 @@ let interp_entry_name interp symb = let get_tactic_entry n = if Int.equal n 0 then - Tactic.simple_tactic, None + Pltac.simple_tactic, None else if Int.equal n 5 then - Tactic.binder_tactic, None + Pltac.binder_tactic, None else if 1<=n && n<5 then - Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) + Pltac.tactic_expr, Some (Extend.Level (string_of_int n)) else error ("Invalid Tactic Notation level: "^(string_of_int n)^".") @@ -405,7 +405,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (loc, v) in let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram]) + Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram]) (** Command *) @@ -434,7 +434,7 @@ let register_ltac local tacl = in let is_shadowed = try - match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with + match Pcoq.parse_string Pltac.tactic (Id.to_string id) with | Tacexpr.TacArg _ -> false | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) @@ -517,9 +517,9 @@ let print_ltacs () = let () = let open Metasyntax in let entries = [ - AnyEntry Pcoq.Tactic.tactic_expr; - AnyEntry Pcoq.Tactic.binder_tactic; - AnyEntry Pcoq.Tactic.simple_tactic; - AnyEntry Pcoq.Tactic.tactic_arg; + AnyEntry Pltac.tactic_expr; + AnyEntry Pltac.binder_tactic; + AnyEntry Pltac.simple_tactic; + AnyEntry Pltac.tactic_arg; ] in register_grammar "tactic" entries |