Replacing some str with strbrk

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 48 insertions, 50 deletions

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
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 61ff69ba7f..1897210210 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -282,7 +282,7 @@ let rec string in_comments bp len = parser
       (parser
         | [< '')'; s >] ->
             if in_comments = Some 0 then
-	      msg_warning (str "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.");
+	      msg_warning (strbr "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.");
             let in_comments = Option.map pred in_comments in
  	    string in_comments bp (store (store len '*') ')') s
         | [< >] ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a3fe0d059c..b6d460a85d 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -490,7 +490,7 @@ and share_names isgoal n l avoid env c t =
         share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
-        if n>0 then msg_warning (str "Detyping.detype: cannot factorize fix enough");
+        if n>0 then msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
         let c = detype isgoal avoid env c in
         let t = detype isgoal avoid env t in
         (List.rev l,c,t)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index e9d6a3c29a..0bd9e95ac4 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -160,7 +160,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
                   (match dest_recarg ra with
 	            | Mrec (_,j) when is_rec -> (depPvect.(j),rest)
 	            | Imbr _  ->
-		        Flags.if_warn msg_warning (str "Ignoring recursive call");
+		        Flags.if_warn msg_warning (strbrk "Ignoring recursive call");
 		        (None,rest)
                     | _ -> (None, rest))
 	  in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 1e73e26342..77d9cd963a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -273,7 +273,7 @@ let rec pat_of_raw metas vars = function
       PMeta None
   | GCast (_,c,_) ->
       Flags.if_warn
-        Pp.msg_warning (str "Cast not taken into account in constr pattern");
+        Pp.msg_warning (strbrk "Cast not taken into account in constr pattern");
       pat_of_raw metas vars c
   | GIf (_,c,(_,None),b1,b2) ->
       PIf (pat_of_raw metas vars c,
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e2b03d0f22..7cecec1578 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -245,9 +245,9 @@ let compute_canonical_projections (con,ind) =
                    if Flags.is_verbose () then
                      (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con)
                       and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in
-		      msg_warning (str "No global reference exists for projection value"
-                                   ++ Termops.print_constr t ++ str " in instance "  
-                                   ++ con_pp ++ str " of " ++ proji_sp_pp ++ str ", ignoring it."));
+		      msg_warning (strbrk "No global reference exists for projection value"
+                                   ++ Termops.print_constr t ++ strbrk " in instance "  
+                                   ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it."));
 		   l
 	       end
 	   | _ -> l)
@@ -279,9 +279,9 @@ let open_canonical_structure i (_,o) =
               and new_can_s = (Termops.print_constr s.o_DEF) in
               let prj = (Nametab.pr_global_env Idset.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
-              msg_warning (str "Ignoring canonical projection to " ++ hd_val
-                             ++ str " by " ++ prj ++ str " in "
-                             ++ new_can_s ++ str ": redundant with " ++ old_can_s)) lo
+              msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val
+                             ++ strbrk " by " ++ prj ++ strbrk " in "
+                             ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo
 
 let cache_canonical_structure o =
   open_canonical_structure 1 o
diff --git a/printing/printer.ml b/printing/printer.ml
index 54e78a7163..d697ab9335 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -480,7 +480,7 @@ let pr_prim_rule = function
       (str"fix " ++ pr_id f ++ str"/" ++ int n)
 
   | FixRule (f,n,others,j) ->
-      if j<>0 then msg_warning (str "Unsupported printing of \"fix\"");
+      if j<>0 then msg_warning (strbrk "Unsupported printing of \"fix\"");
       let rec print_mut = function
 	| (f,n,ar)::oth ->
            pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
@@ -492,7 +492,7 @@ let pr_prim_rule = function
       (str"cofix " ++ pr_id f)
 
   | Cofix (f,others,j) ->
-      if j<>0 then msg_warning (str "Unsupported printing of \"fix\"");
+      if j<>0 then msg_warning (strbrk "Unsupported printing of \"fix\"");
       let rec print_mut = function
 	| (f,ar)::oth ->
 	  (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 336c451d04..45e48a9d78 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -236,7 +236,7 @@ let add_tactic s t =
 let overwriting_add_tactic s t =
   if Hashtbl.mem tac_tab s then begin
     Hashtbl.remove tac_tab s;
-    msg_warning (str ("Overwriting definition of tactic "^s))
+    msg_warning (strbrk ("Overwriting definition of tactic "^s))
   end;
   Hashtbl.add tac_tab s t
 
@@ -274,7 +274,7 @@ let lookup_genarg id =
   try Gmap.find id !extragenargtab
   with Not_found ->
     let msg = "No interpretation function found for entry " ^ id in
-    msg_warning (str msg);
+    msg_warning (strbrk msg);
     let f = (fun _ _ -> failwith msg), (fun _ _ _ -> failwith msg), (fun _ a -> a) in
     add_interp_genarg id f;
     f
@@ -1820,9 +1820,8 @@ and eval_tactic ist = function
   | TacArg a -> interp_tactic ist (TacArg a)
   | TacInfo tac ->
       msg_warning
-	(str "The general \"info\" tactic is currently not working.\n" ++
-	 str "Some specific verbose tactics may exist instead, such as\n" ++
-	 str "info_trivial, info_auto, info_eauto.");
+	(strbrk "The general \"info\" tactic is currently not working." ++ fnl () ++
+	 strbrk "Some specific verbose tactics may exist instead, such as info_trivial, info_auto, info_eauto.");
       eval_tactic ist tac
 
 and force_vrec ist gl = function
@@ -2775,7 +2774,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
-    msg_warning (str "The reference " ++ pr_global ref ++ str " is not " ++
+    msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++
           str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++
           pr_global ref') ;
    ref'
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f4f6cefff6..b324a03be3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -91,8 +91,8 @@ let interp_definition bl red_option c ctypopt =
 	let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in
 	(* Check that all implicit arguments inferable from the term is inferable from the type *)
 	if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false)
-	then msg_warning (str "Implicit arguments declaration relies on type." ++
-		     spc () ++ str "The term declares more implicits than the type here.");
+	then msg_warning (strbrk "Implicit arguments declaration relies on type." ++
+		     spc () ++ strbrk "The term declares more implicits than the type here.");
 	imps1@(Impargs.lift_implicits nb_args impsty),
 	{ const_entry_body = body;
           const_entry_secctx = None;
@@ -112,7 +112,7 @@ let declare_global_definition ident ce local k imps =
   let gr = ConstRef kn in
     maybe_declare_manual_implicits false gr imps;
     if local = Local && Flags.is_verbose() then
-      msg_warning (pr_id ident ++ str" is declared as a global definition");
+      msg_warning (pr_id ident ++ strbrk " is declared as a global definition");
     definition_message ident;
     Autoinstance.search_declaration (ConstRef kn);
     gr
@@ -131,8 +131,8 @@ let declare_definition ident (local,k) ce imps hook =
         definition_message ident;
         if Pfedit.refining () then
           Flags.if_warn msg_warning
-	    (str"Local definition " ++ pr_id ident ++
-             str" is not visible from current goals");
+	    (strbrk "Local definition " ++ pr_id ident ++
+             strbrk " is not visible from current goals");
         VarRef ident
     | (Global|Local) ->
         declare_global_definition ident ce local k imps in
@@ -167,8 +167,8 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
             (Lib.cwd(), SectionLocalAssum (c,impl), IsAssumption kind) in
         assumption_message ident;
         if is_verbose () & Pfedit.refining () then
-          msg_warning (str"Variable " ++ pr_id ident ++
-          str" is not visible from current goals");
+          msg_warning (str"Variable" ++ spc () ++ pr_id ident ++
+          strbrk " is not visible from current goals");
 	let r = VarRef ident in
 	  Typeclasses.declare_instance None true r; r
     | (Global|Local) ->
@@ -179,8 +179,8 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) =
 	  maybe_declare_manual_implicits false gr imps;
         assumption_message ident;
         if local=Local & Flags.is_verbose () then
-          msg_warning (pr_id ident ++ str" is declared as a parameter" ++
-          str" because it is at a global level");
+          msg_warning (pr_id ident ++ strbrk " is declared as a parameter" ++
+          strbrk " because it is at a global level");
 	Autoinstance.search_declaration (ConstRef kn);
 	Typeclasses.declare_instance None false gr;
         gr 
@@ -290,7 +290,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
 
   (* Instantiate evars and check all are resolved *)
   let evd = consider_remaining_unif_problems env_params !evdref in
-  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env_params evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env_params evd in
   let sigma = evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
@@ -781,7 +781,7 @@ let interp_recursive isfix fixl notations =
   (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
 
 let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) =
-  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in
   List.iter (Option.iter (check_evars (push_named_context rec_sign env) Evd.empty evd)) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
   if not (List.mem None fixdefs) then begin
@@ -889,8 +889,7 @@ let do_program_recursive fixkind fixl ntns =
   in
     (* Program-specific code *)
     (* Get the interesting evars, those that were not instanciated *)
-  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals_or_obligations ~fail:true env evd in
-  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:false env evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in
     (* Solve remaining evars *)
   let rec collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6bbe6b026b..860ef2e61c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -128,8 +128,8 @@ let compile_files () =
 let set_compat_version = function
   | "8.3" -> compat_version := Some V8_3
   | "8.2" -> compat_version := Some V8_2
-  | "8.1" -> msg_warning (str "Compatibility with version 8.1 not supported.")
-  | "8.0" -> msg_warning (str "Compatibility with version 8.0 not supported.")
+  | "8.1" -> msg_warning (strbrk "Compatibility with version 8.1 not supported.")
+  | "8.0" -> msg_warning (strbrk "Compatibility with version 8.0 not supported.")
   | s -> error ("Unknown compatibility version \""^s^"\".")
 
 (*s options for the virtual machine *)
@@ -153,7 +153,7 @@ let usage () =
   flush stderr ;
   exit 1
 
-let warning s = msg_warning (str s)
+let warning s = msg_warning (strbrk s)
 
 let ide_slave = ref false
 let filter_opts = ref false
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 9d5d7d7193..5ffbedcd7e 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -105,9 +105,9 @@ let coqide_cmd_checks (loc,ast) =
   if Vernac.is_navigation_vernac ast then
     user_error "Use CoqIDE navigation instead";
   if is_undo ast then
-    msg_warning (str "Rather use CoqIDE navigation instead");
+    msg_warning (strbrk "Rather use CoqIDE navigation instead");
   if is_query ast then
-    msg_warning (str "Query commands should not be inserted in scripts")
+    msg_warning (strbrk "Query commands should not be inserted in scripts")
 
 (** Interpretation (cf. [Ide_intf.interp]) *)
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 6537ff10d7..dc3e0dc474 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -282,7 +282,7 @@ let declare_congr_scheme ind =
     then
       ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
     else
-      msg_warning (str "Cannot build congruence scheme because eq is not found")
+      msg_warning (strbrk "Cannot build congruence scheme because eq is not found")
   end
 
 let declare_sym_scheme ind =
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 74b9ebe26b..fe1cd7eb32 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -602,7 +602,7 @@ let is_not_small_constr = function
 let rec define_keywords_aux = function
   | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
       when is_not_small_constr e ->
-      msg_info (str ("Identifier '"^k^"' now a keyword"));
+      msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
       Lexer.add_keyword k;
       n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | n :: l -> n :: define_keywords_aux l
@@ -611,7 +611,7 @@ let rec define_keywords_aux = function
   (* Ensure that IDENT articulation terminal symbols are keywords *)
 let define_keywords = function
   | GramConstrTerminal(IDENT k)::l ->
-      msg_info (str ("Identifier '"^k^"' now a keyword"));
+      msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
       Lexer.add_keyword k;
       GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
   | l -> define_keywords_aux l
@@ -854,7 +854,7 @@ let check_rule_productivity l =
     error "A recursive notation must start with at least one symbol."
 
 let is_not_printable = function
-  | NVar _ -> msg_warning (str "This notation will not be used for printing as it is bound to a single variable."); true
+  | NVar _ -> msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable."); true
   | _ -> false
 
 let find_precedence lev etyps symbols =
@@ -865,7 +865,7 @@ let find_precedence lev etyps symbols =
 	    error "The level of the leftmost non-terminal cannot be changed."
 	| ETName | ETBigint | ETReference ->
 	    if lev = None then
-	      ([msg_info,str "Setting notation at level 0."],0)
+	      ([msg_info,strbrk "Setting notation at level 0."],0)
 	    else
 	    if lev <> Some 0 then
 	      error "A notation starting with an atomic expression must be at level 0."
@@ -885,7 +885,7 @@ let find_precedence lev etyps symbols =
       (match list_last symbols with Terminal _ -> true |_ -> false)
       ->
       if lev = None then
-	([msg_info,str "Setting notation at level 0."], 0)
+	([msg_info,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
   | _ ->
       if lev = None then error "Cannot determine the level.";
@@ -912,7 +912,7 @@ let remove_curly_brackets l =
             (match next' with
               | Terminal "}" as t2 :: l'' as l1 ->
                   if l <> l0 or l' <> l1 then
-                    msg_warning (str "Skipping spaces inside curly brackets");
+                    msg_warning (strbrk "Skipping spaces inside curly brackets");
                   if deb & l'' = [] then [t1;x;t2] else begin
                     check_curly_brackets_notation_exists ();
                     x :: aux false l''
@@ -957,7 +957,7 @@ let compute_pure_syntax_data (df,mods) =
   let msgs =
     if onlyparse then
       (msg_warning,
-      str "The only parsing modifier has no effect in Reserved Notation.")::msgs
+      strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
   msgs, sy_data