diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/autorewrite.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 4981e70333..e9a852455d 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -91,7 +91,7 @@ let find_matches bas pat = List.map (fun ((_,rew), esubst, subst) -> rew) res let print_rewrite_hintdb bas = - ppnl (str "Database " ++ str bas ++ (Pp.cut ()) ++ + (str "Database " ++ str bas ++ (Pp.cut ()) ++ prlist_with_sep Pp.cut (fun h -> str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++ diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index a3fc729595..e5ec949ed4 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -39,7 +39,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> tac val auto_multi_rewrite_with : ?conds:conditions -> tactic -> string list -> Locus.clause -> tactic -val print_rewrite_hintdb : string -> unit +val print_rewrite_hintdb : string -> Pp.std_ppcmds open Clenv diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a628fe26a0..336c451d04 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2775,7 +2775,7 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (eq_constr (constr_of_global ref') t') then - ppnl (str "Warning: The reference " ++ pr_global ref ++ str " is not " ++ + msg_warning (str "The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; ref' |