From 0f500f2e7a3164df44a2b20e67550cb0072d8948 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 4 Jun 2012 17:18:31 +0000
Subject: Replacing some str with strbrk

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/implicit_quantifiers.ml | 4 ++--
 interp/notation.ml             | 6 +++---
 interp/topconstr.ml            | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'interp')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 90b495982e..9389a1690b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -315,8 +315,8 @@ let implicits_of_glob_constr ?(with_products=true) l =
 	  if with_products then abs na bk b
 	  else 
 	    (if bk = Implicit then
-	       msg_warning (str "Ignoring implicit status of product binder " ++ 
-			      pr_name na ++ str " and following binders");
+	       msg_warning (strbrk "Ignoring implicit status of product binder " ++ 
+			      pr_name na ++ strbrk " and following binders");
 	     [])
       | GLambda (loc, na, bk, t, b) -> abs na bk b
       | GLetIn (loc, na, t, b) -> aux i b
diff --git a/interp/notation.ml b/interp/notation.ml
index 64911675b8..2430b980ca 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -156,14 +156,14 @@ let declare_delimiters scope key =
     | Some oldkey when oldkey = key -> ()
     | Some oldkey ->
 	Flags.if_warn msg_warning
-	  (str ("Overwriting previous delimiting key "^oldkey^" in scope "^scope));
+	  (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope));
 	scope_map := Gmap.add scope newsc !scope_map
   end;
   try
     let oldscope = Gmap.find key !delimiters_map in
     if oldscope = scope then ()
     else begin
-      Flags.if_warn msg_warning (str ("Hiding binding of key "^key^" to "^oldscope));
+      Flags.if_warn msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope));
       delimiters_map := Gmap.add key scope !delimiters_map
     end
   with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map
@@ -317,7 +317,7 @@ let declare_notation_interpretation ntn scopt pat df =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
   if Gmap.mem ntn sc.notations then
-    Flags.if_warn msg_warning (str ("Notation "^ntn^" was already used"^
+    Flags.if_warn msg_warning (strbrk ("Notation "^ntn^" was already used"^
     (if scopt = None then "" else " in scope "^scope)));
   let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in
   scope_map := Gmap.add scope sc !scope_map;
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 1036baf7c1..9b3c00bf22 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -138,7 +138,7 @@ let fold_constr_expr_with_binders g f n acc = function
 	fold_local_binders g f n'
 	  (fold_local_binders g f n acc t lb) c lb) l acc
   | CCoFix (loc,_,_) ->
-      msg_warning (str "Capture check in multiple binders not done"); acc
+      msg_warning (strbrk "Capture check in multiple binders not done"); acc
 
 let free_vars_of_constr_expr c =
   let rec aux bdvars l = function
-- 
cgit v1.2.3