diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-27 14:58:03 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-07-27 15:39:10 +0200 |
| commit | b52dca14d3ac66ecd1657a21fecd0b48751096a7 (patch) | |
| tree | 193b1f22f433b24dd8038e54c2e96041acc6dd19 /printing | |
| 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')
| -rw-r--r-- | printing/pptactic.ml | 7 | ||||
| -rw-r--r-- | printing/pptactic.mli | 8 |
2 files changed, 10 insertions, 5 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 04e1a4923..381534d6d 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -260,7 +260,12 @@ let pr_extend_gen pr_gen lev s l = let p = pr_tacarg_using_rule pr_gen (pl,l) in if lev' > lev then surround p else p with Not_found -> - str "<" ++ str s ++ str ">" ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)" + let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in + let args = match l with + | [] -> mt () + | _ -> spc() ++ pr_sequence pr_gen l + in + str "<" ++ name ++ str ">" ++ args let pr_alias_gen pr_gen lev key l = try diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 82cb9c0a5..6c2f43cb6 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 |