diff options
| author | Pierre-Marie Pédrot | 2014-07-27 14:58:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-27 15:39:10 +0200 |
| commit | b52dca14d3ac66ecd1657a21fecd0b48751096a7 (patch) | |
| tree | 193b1f22f433b24dd8038e54c2e96041acc6dd19 /printing/pptactic.mli | |
| parent | 0736cd1ff1eb07c6faae43cdfbe2efd11c8470e9 (diff) | |
Qualified ML tactic names. The plugin name is used to discriminate
potentially conflicting tactics names from different plugins.
Diffstat (limited to 'printing/pptactic.mli')
| -rw-r--r-- | printing/pptactic.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 82cb9c0a58..6c2f43cb68 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -51,7 +51,7 @@ type pp_tactic = { pptac_prods : int * grammar_terminals; } -val declare_ml_tactic_pprule : string -> pp_tactic -> unit +val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_clauses : bool option -> @@ -83,19 +83,19 @@ val pr_raw_extend: (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> int -> - string -> raw_generic_argument list -> std_ppcmds + ml_tactic_name -> raw_generic_argument list -> std_ppcmds val pr_glob_extend: (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> (glob_constr_pattern_and_expr -> std_ppcmds) -> int -> - string -> glob_generic_argument list -> std_ppcmds + ml_tactic_name -> glob_generic_argument list -> std_ppcmds val pr_extend : (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> (constr_pattern -> std_ppcmds) -> int -> - string -> typed_generic_argument list -> std_ppcmds + ml_tactic_name -> typed_generic_argument list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds |