Fix unescaped end-of-lines (OCaml warning 29)

See http://caml.inria.fr/mantis/view.php?id=4940

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

3 files changed, 59 insertions, 59 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 2f89c59851..efaf7707c3 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -365,7 +365,7 @@ let error_not_same_scope x y =
 
 let error_both_bound_and_binding x y =
   errorlabstrm "" (strbrk "The recursive variables " ++ pr_id x ++
-  strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder
+  strbrk " and " ++ pr_id y ++ strbrk " cannot be used as placeholder \
   for both terms and binders.")
 
 (**********************************************************************)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index a3dbff23c1..fc4d18b57d 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -18,58 +18,58 @@ let print_usage_channel co command =
   output_string co command;
   output_string co "Coq options are:\n";
   output_string co
-"  -I dir -as coqdir      map physical dir to logical coqdir
-  -I dir                 map directory dir to the empty logical path
-  -include dir           (idem)
-  -R dir -as coqdir      recursively map physical dir to logical coqdir
-  -R dir coqdir          (idem)
-  -top coqdir            set the toplevel name to be coqdir instead of Top
-  -notop    r            set the toplevel name to be the empty logical path
-  -exclude-dir f         exclude subdirectories named f for option -R
-
-  -inputstate f          read state from file f.coq
-  -is f                  (idem)
-  -nois                  start with an empty state
-  -outputstate f         write state in file f.coq
-  -compat X.Y            provides compatibility support for Coq version X.Y
-
-  -load-ml-object f      load ML object file f
-  -load-ml-source f      load ML file f
-  -load-vernac-source f  load Coq file f.v (Load f.)
-  -l f                   (idem)
-  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)
-  -lv f	                 (idem)
-  -load-vernac-object f  load Coq object file f.vo
-  -require f             load Coq object file f.vo and import it (Require f.)
-  -compile f             compile Coq file f.v (implies -batch)
-  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)
-
-  -opt                   run the native-code version of Coq
-  -byte                  run the bytecode version of Coq
-
-  -where                 print Coq's standard library location and exit
-  -config                print Coq's configuration information and exit
-  -v                     print Coq version and exit
-
-  -q                     skip loading of rcfile
-  -init-file f           set the rcfile to f
-  -user u                use the rcfile of user u
-  -batch                 batch mode (exits just after arguments parsing)
-  -boot                  boot mode (implies -q and -batch)
-  -emacs                 tells Coq it is executed under Emacs
-  -noglob                do not dump globalizations
-  -dump-glob f           dump globalizations in file f (to be used by coqdoc)
-  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
-  -impredicative-set     set sort Set impredicative
-  -load-proofs           load opaque proofs in memory (default)
-  -dont-load-proofs      don't load opaque proofs in memory 
-  -xml                   export XML files either to the hierarchy rooted in
-                         the directory $COQ_XML_LIBRARY_ROOT (if set) or to
-                         stdout (if unset)
-  -quality               improve the legibility of the proof terms produced by
-                         some tactics
-  -h, --help             print this list of options
-"
+"  -I dir -as coqdir      map physical dir to logical coqdir\
+\n  -I dir                 map directory dir to the empty logical path\
+\n  -include dir           (idem)\
+\n  -R dir -as coqdir      recursively map physical dir to logical coqdir\
+\n  -R dir coqdir          (idem)\
+\n  -top coqdir            set the toplevel name to be coqdir instead of Top\
+\n  -notop    r            set the toplevel name to be the empty logical path\
+\n  -exclude-dir f         exclude subdirectories named f for option -R\
+\n\
+\n  -inputstate f          read state from file f.coq\
+\n  -is f                  (idem)\
+\n  -nois                  start with an empty state\
+\n  -outputstate f         write state in file f.coq\
+\n  -compat X.Y            provides compatibility support for Coq version X.Y\
+\n\
+\n  -load-ml-object f      load ML object file f\
+\n  -load-ml-source f      load ML file f\
+\n  -load-vernac-source f  load Coq file f.v (Load f.)\
+\n  -l f                   (idem)\
+\n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose f.)\
+\n  -lv f	                 (idem)\
+\n  -load-vernac-object f  load Coq object file f.vo\
+\n  -require f             load Coq object file f.vo and import it (Require f.)\
+\n  -compile f             compile Coq file f.v (implies -batch)\
+\n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
+\n\
+\n  -opt                   run the native-code version of Coq\
+\n  -byte                  run the bytecode version of Coq\
+\n\
+\n  -where                 print Coq's standard library location and exit\
+\n  -config                print Coq's configuration information and exit\
+\n  -v                     print Coq version and exit\
+\n\
+\n  -q                     skip loading of rcfile\
+\n  -init-file f           set the rcfile to f\
+\n  -user u                use the rcfile of user u\
+\n  -batch                 batch mode (exits just after arguments parsing)\
+\n  -boot                  boot mode (implies -q and -batch)\
+\n  -emacs                 tells Coq it is executed under Emacs\
+\n  -noglob                do not dump globalizations\
+\n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
+\n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
+\n  -impredicative-set     set sort Set impredicative\
+\n  -load-proofs           load opaque proofs in memory (default)\
+\n  -dont-load-proofs      don't load opaque proofs in memory\
+\n  -xml                   export XML files either to the hierarchy rooted in\
+\n                         the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
+\n                         stdout (if unset)\
+\n  -quality               improve the legibility of the proof terms produced by\
+\n                         some tactics\
+\n  -h, --help             print this list of options\
+\n"
 
 (* print the usage on standard error *)
 
@@ -79,11 +79,11 @@ let print_usage_coqtop () =
   print_usage "Usage: coqtop <options>\n\n"
 
 let print_usage_coqc () =
-  print_usage "Usage: coqc <options> <Coq options> file...\n
-options are:
-  -verbose  compile verbosely
-  -image f  specify an alternative executable for Coq
-  -t        keep temporary files\n\n"
+  print_usage "Usage: coqc <options> <Coq options> file...\n\
+\noptions are:\
+\n  -verbose  compile verbosely\
+\n  -image f  specify an alternative executable for Coq\
+\n  -t        keep temporary files\n\n"
 
 (* Print the configuration information *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d785a8a406..c5125e9ff1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1128,7 +1128,7 @@ let interp_search_about_item = function
 	    (fun _ -> true) s sc in
 	GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
-	error ("Unable to interp \""^s^"\" either as a reference or
+	error ("Unable to interp \""^s^"\" either as a reference or \
           	as an identifier component")
 
 let vernac_search s r =