From 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 1 Jun 2012 19:53:57 +0000
Subject: Cleaning Pp.ppnl use

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/autorewrite.ml  | 2 +-
 tactics/autorewrite.mli | 2 +-
 tactics/tacinterp.ml    | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

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'
-- 
cgit v1.2.3