diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 19:53:57 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 19:53:57 +0000 |
| commit | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (patch) | |
| tree | 75f2746f738c2b2c111b701f80d59d10f80c75f7 /tactics | |
| parent | cf7660a3a8932ee593a376e8ec7ec251896a72e3 (diff) | |
Cleaning Pp.ppnl use
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 85f007b7-540e-0410-9357-904b9bb8a0f7
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 4981e7033..e9a852455 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 a3fc72959..e5ec949ed 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 a628fe26a..336c451d0 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' |