Replacing some str with strbrk

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

5 files changed, 25 insertions, 26 deletions

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