From b20d52da0d040fe37bb75b0b739ad7686f9af127 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 22 Apr 2017 12:55:46 +0200
Subject: Warning 29: non escaped end of line may be non portable

---
 ide/coqide_ui.ml       | 284 ++++++++++++++++++++++++-------------------------
 ide/ide_slave.ml       |   4 +-
 interp/constrintern.ml |   6 +-
 tools/coq_makefile.ml  | 116 ++++++++++----------
 toplevel/usage.ml      |   2 +-
 5 files changed, 206 insertions(+), 206 deletions(-)

diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 2ae18593ac..91c281c8d8 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -28,148 +28,148 @@ let list_queries menu li =
   res_buf
 
 let init () =
-  let theui = Printf.sprintf "<ui>
-<menubar name='CoqIde MenuBar'>
-  <menu action='File'>
-    <menuitem action='New' />
-    <menuitem action='Open' />
-    <menuitem action='Save' />
-    <menuitem action='Save as' />
-    <menuitem action='Save all' />
-    <menuitem action='Revert all buffers' />
-    <menuitem action='Close buffer' />
-    <menuitem action='Print...' />
-    <menu action='Export to'>
-      <menuitem action='Html' />
-      <menuitem action='Latex' />
-      <menuitem action='Dvi' />
-      <menuitem action='Pdf' />
-      <menuitem action='Ps' />
-    </menu>
-    <menuitem action='Rehighlight' />
-    %s
-  </menu>
-  <menu name='Edit' action='Edit'>
-    <menuitem action='Undo' />
-    <menuitem action='Redo' />
-    <separator />
-    <menuitem action='Cut' />
-    <menuitem action='Copy' />
-    <menuitem action='Paste' />
-    <separator />
-    <menuitem action='Find' />
-    <menuitem action='Find Next' />
-    <menuitem action='Find Previous' />
-    <menuitem action='Complete Word' />
-    <separator />
-    <menuitem action='External editor' />
-    <separator />
-    <menuitem name='Prefs' action='Preferences' />
-  </menu>
-  <menu name='View' action='View'>
-    <menuitem action='Previous tab' />
-    <menuitem action='Next tab' />
-    <separator/>
-    <menuitem action='Zoom in' />
-    <menuitem action='Zoom out' />
-    <menuitem action='Zoom fit' />
-    <separator/>
-    <menuitem action='Show Toolbar' />
-    <menuitem action='Query Pane' />
-    <separator/>
-    <menuitem action='Display implicit arguments' />
-    <menuitem action='Display coercions' />
-    <menuitem action='Display raw matching expressions' />
-    <menuitem action='Display notations' />
-    <menuitem action='Display all basic low-level contents' />
-    <menuitem action='Display existential variable instances' />
-    <menuitem action='Display universe levels' />
-    <menuitem action='Display all low-level contents' />
-  </menu>
-  <menu action='Navigation'>
-    <menuitem action='Forward' />
-    <menuitem action='Backward' />
-    <menuitem action='Go to' />
-    <menuitem action='Start' />
-    <menuitem action='End' />
-    <menuitem action='Interrupt' />
-    <menuitem action='Previous' />
-    <menuitem action='Next' />
-  </menu>
-  <menu action='Try Tactics'>
-    <menuitem action='auto' />
-    <menuitem action='auto with *' />
-    <menuitem action='eauto' />
-    <menuitem action='eauto with *' />
-    <menuitem action='intuition' />
-    <menuitem action='omega' />
-    <menuitem action='simpl' />
-    <menuitem action='tauto' />
-    <menuitem action='trivial' />
-    <menuitem action='Wizard' />
-    <separator />
-    %s
-  </menu>
-  <menu action='Templates'>
-    <menuitem action='Lemma' />
-    <menuitem action='Theorem' />
-    <menuitem action='Definition' />
-    <menuitem action='Inductive' />
-    <menuitem action='Fixpoint' />
-    <menuitem action='Scheme' />
-    <menuitem action='match' />
-    <separator />
-    %s
-  </menu>
-  <menu action='Queries'>
-    <menuitem action='Search' />
-    <menuitem action='Check' />
-    <menuitem action='Print' />
-    <menuitem action='About' />
-    <menuitem action='Locate' />
-    <menuitem action='Print Assumptions' />
-    <separator />
-    %s
-  </menu>
-  <menu name='Tools' action='Tools'>
-    <menuitem action='Comment' />
-    <menuitem action='Uncomment' />
-    <separator />
-    <menuitem action='Coqtop arguments' />
-  </menu>
-  <menu action='Compile'>
-    <menuitem action='Compile buffer' />
-    <menuitem action='Make' />
-    <menuitem action='Next error' />
-    <menuitem action='Make makefile' />
-  </menu>
-  <menu action='Windows'>
-    <menuitem action='Detach View' />
-  </menu>
-  <menu name='Help' action='Help'>
-    <menuitem action='Browse Coq Manual' />
-    <menuitem action='Browse Coq Library' />
-    <menuitem action='Help for keyword' />
-    <menuitem action='Help for μPG mode' />
-    <separator />
-    <menuitem name='Abt' action='About Coq' />
-  </menu>
-</menubar>
-<toolbar name='CoqIde ToolBar'>
-  <toolitem action='Save' />
-  <toolitem action='Close buffer' />
-  <toolitem action='Forward' />
-  <toolitem action='Backward' />
-  <toolitem action='Go to' />
-  <toolitem action='Start' />
-  <toolitem action='End' />
-  <toolitem action='Force' />
-  <toolitem action='Interrupt' />
-  <toolitem action='Previous' />
-  <toolitem action='Next' />
-  <toolitem action='Wizard' />
-</toolbar>
-</ui>"
+  let theui = Printf.sprintf "<ui>\
+\n<menubar name='CoqIde MenuBar'>\
+\n  <menu action='File'>\
+\n    <menuitem action='New' />\
+\n    <menuitem action='Open' />\
+\n    <menuitem action='Save' />\
+\n    <menuitem action='Save as' />\
+\n    <menuitem action='Save all' />\
+\n    <menuitem action='Revert all buffers' />\
+\n    <menuitem action='Close buffer' />\
+\n    <menuitem action='Print...' />\
+\n    <menu action='Export to'>\
+\n      <menuitem action='Html' />\
+\n      <menuitem action='Latex' />\
+\n      <menuitem action='Dvi' />\
+\n      <menuitem action='Pdf' />\
+\n      <menuitem action='Ps' />\
+\n    </menu>\
+\n    <menuitem action='Rehighlight' />\
+\n    %s\
+\n  </menu>\
+\n  <menu name='Edit' action='Edit'>\
+\n    <menuitem action='Undo' />\
+\n    <menuitem action='Redo' />\
+\n    <separator />\
+\n    <menuitem action='Cut' />\
+\n    <menuitem action='Copy' />\
+\n    <menuitem action='Paste' />\
+\n    <separator />\
+\n    <menuitem action='Find' />\
+\n    <menuitem action='Find Next' />\
+\n    <menuitem action='Find Previous' />\
+\n    <menuitem action='Complete Word' />\
+\n    <separator />\
+\n    <menuitem action='External editor' />\
+\n    <separator />\
+\n    <menuitem name='Prefs' action='Preferences' />\
+\n  </menu>\
+\n  <menu name='View' action='View'>\
+\n    <menuitem action='Previous tab' />\
+\n    <menuitem action='Next tab' />\
+\n    <separator/>\
+\n    <menuitem action='Zoom in' />\
+\n    <menuitem action='Zoom out' />\
+\n    <menuitem action='Zoom fit' />\
+\n    <separator/>\
+\n    <menuitem action='Show Toolbar' />\
+\n    <menuitem action='Query Pane' />\
+\n    <separator/>\
+\n    <menuitem action='Display implicit arguments' />\
+\n    <menuitem action='Display coercions' />\
+\n    <menuitem action='Display raw matching expressions' />\
+\n    <menuitem action='Display notations' />\
+\n    <menuitem action='Display all basic low-level contents' />\
+\n    <menuitem action='Display existential variable instances' />\
+\n    <menuitem action='Display universe levels' />\
+\n    <menuitem action='Display all low-level contents' />\
+\n  </menu>\
+\n  <menu action='Navigation'>\
+\n    <menuitem action='Forward' />\
+\n    <menuitem action='Backward' />\
+\n    <menuitem action='Go to' />\
+\n    <menuitem action='Start' />\
+\n    <menuitem action='End' />\
+\n    <menuitem action='Interrupt' />\
+\n    <menuitem action='Previous' />\
+\n    <menuitem action='Next' />\
+\n  </menu>\
+\n  <menu action='Try Tactics'>\
+\n    <menuitem action='auto' />\
+\n    <menuitem action='auto with *' />\
+\n    <menuitem action='eauto' />\
+\n    <menuitem action='eauto with *' />\
+\n    <menuitem action='intuition' />\
+\n    <menuitem action='omega' />\
+\n    <menuitem action='simpl' />\
+\n    <menuitem action='tauto' />\
+\n    <menuitem action='trivial' />\
+\n    <menuitem action='Wizard' />\
+\n    <separator />\
+\n    %s\
+\n  </menu>\
+\n  <menu action='Templates'>\
+\n    <menuitem action='Lemma' />\
+\n    <menuitem action='Theorem' />\
+\n    <menuitem action='Definition' />\
+\n    <menuitem action='Inductive' />\
+\n    <menuitem action='Fixpoint' />\
+\n    <menuitem action='Scheme' />\
+\n    <menuitem action='match' />\
+\n    <separator />\
+\n    %s\
+\n  </menu>\
+\n  <menu action='Queries'>\
+\n    <menuitem action='Search' />\
+\n    <menuitem action='Check' />\
+\n    <menuitem action='Print' />\
+\n    <menuitem action='About' />\
+\n    <menuitem action='Locate' />\
+\n    <menuitem action='Print Assumptions' />\
+\n    <separator />\
+\n    %s\
+\n  </menu>\
+\n  <menu name='Tools' action='Tools'>\
+\n    <menuitem action='Comment' />\
+\n    <menuitem action='Uncomment' />\
+\n    <separator />\
+\n    <menuitem action='Coqtop arguments' />\
+\n  </menu>\
+\n  <menu action='Compile'>\
+\n    <menuitem action='Compile buffer' />\
+\n    <menuitem action='Make' />\
+\n    <menuitem action='Next error' />\
+\n    <menuitem action='Make makefile' />\
+\n  </menu>\
+\n  <menu action='Windows'>\
+\n    <menuitem action='Detach View' />\
+\n  </menu>\
+\n  <menu name='Help' action='Help'>\
+\n    <menuitem action='Browse Coq Manual' />\
+\n    <menuitem action='Browse Coq Library' />\
+\n    <menuitem action='Help for keyword' />\
+\n    <menuitem action='Help for μPG mode' />\
+\n    <separator />\
+\n    <menuitem name='Abt' action='About Coq' />\
+\n  </menu>\
+\n</menubar>\
+\n<toolbar name='CoqIde ToolBar'>\
+\n  <toolitem action='Save' />\
+\n  <toolitem action='Close buffer' />\
+\n  <toolitem action='Forward' />\
+\n  <toolitem action='Backward' />\
+\n  <toolitem action='Go to' />\
+\n  <toolitem action='Start' />\
+\n  <toolitem action='End' />\
+\n  <toolitem action='Force' />\
+\n  <toolitem action='Interrupt' />\
+\n  <toolitem action='Previous' />\
+\n  <toolitem action='Next' />\
+\n  <toolitem action='Wizard' />\
+\n</toolbar>\
+\n</ui>"
     (if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
     (Buffer.contents (list_items "Tactic" Coq_commands.tactics))
     (Buffer.contents (list_items "Template" Coq_commands.commands))
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index ca0ef38d32..dbfe4256b3 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -512,5 +512,5 @@ let () = Coqtop.toploop_init := (fun args ->
 let () = Coqtop.toploop_run := loop
 
 let () = Usage.add_to_usage "coqidetop"
-"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format
-  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
+"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
+\n  --help-XML-protocol    print the documentation of the XML protocol used by CoqIDE\n"
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 389880c5c5..3f99a3c7c0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -855,9 +855,9 @@ let intern_qualid loc qid intern env lvar us args =
       | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
          GApp (loc, GRef (loc', ref, us), arg)
       | Some _, _ ->
-        user_err ~loc  (str "Notation " ++ pr_qualid qid ++
-          str " cannot have a universe instance, its expanded head
-               does not start with a reference")
+        user_err ~loc  (str "Notation " ++ pr_qualid qid
+                        ++ str " cannot have a universe instance,"
+                        ++ str " its expanded head does not start with a reference")
       in
       c, projapp, args2
 
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index ed89bda2cf..4875cb62bf 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -56,48 +56,48 @@ let lib_dirs =
 
 
 let usage () =
-  output_string stderr "Usage summary:
-
-coq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]
-  ... [any] ... [-extra[-phony] result dependencies command]
-  ... [-I dir] ... [-R physicalpath logicalpath]
-  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]
-  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]
-  [-h] [--help]
-
-[file.v]: Coq file to be compiled
-[file.ml[i4]?]: Objective Caml file to be compiled
-[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml
-  library/module
-[any] : subdirectory that should be \"made\" and has a Makefile itself
-  to do so. Very fragile and discouraged.
-[-extra result dependencies command]: add target \"result\" with command
-  \"command\" and dependencies \"dependencies\". If \"result\" is not
-  generic (do not contains a %), \"result\" is built by _make all_ and
-  deleted by _make clean_.
-[-extra-phony result dependencies command]: add a PHONY target \"result\"
- with command \"command\" and dependencies \"dependencies\". Note that
- _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as
- as a dependencies of an already defined target \"foo\".
-[-I dir]: look for Objective Caml dependencies in \"dir\"
-[-R physicalpath logicalpath]: look for Coq dependencies resursively
-  starting from \"physicalpath\". The logical path associated to the
-  physical path is \"logicalpath\".
-[-Q physicalpath logicalpath]: look for Coq dependencies starting from
-  \"physicalpath\". The logical path associated to the physical path
-  is \"logicalpath\".
-[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"
-[-byte]: compile with byte-code version of coq
-[-opt]: compile with native-code version of coq
-[-arg opt]: send option \"opt\" to coqc
-[-install opt]: where opt is \"user\" to force install into user directory,
-  \"none\" to build a makefile with no install target or
-  \"global\" to force install in $COQLIB directory
-[-f file]: take the contents of file as arguments
-[-o file]: output should go in file file
-	Output file outside the current directory is forbidden.
-[-h]: print this usage summary
-[--help]: equivalent to [-h]\n";
+  output_string stderr "Usage summary:\
+\n\
+\ncoq_makefile .... [file.v] ... [file.ml[i4]?] ... [file.ml{lib,pack}]\
+\n  ... [any] ... [-extra[-phony] result dependencies command]\
+\n  ... [-I dir] ... [-R physicalpath logicalpath]\
+\n  ... [-Q physicalpath logicalpath] ... [VARIABLE = value]\
+\n  ...  [-arg opt] ... [-opt|-byte] [-no-install] [-f file] [-o file]\
+\n  [-h] [--help]\
+\n\
+\n[file.v]: Coq file to be compiled\
+\n[file.ml[i4]?]: Objective Caml file to be compiled\
+\n[file.ml{lib,pack}]: ocamlbuild file that describes a Objective Caml\
+\n  library/module\
+\n[any] : subdirectory that should be \"made\" and has a Makefile itself\
+\n  to do so. Very fragile and discouraged.\
+\n[-extra result dependencies command]: add target \"result\" with command\
+\n  \"command\" and dependencies \"dependencies\". If \"result\" is not\
+\n  generic (do not contains a %), \"result\" is built by _make all_ and\
+\n  deleted by _make clean_.\
+\n[-extra-phony result dependencies command]: add a PHONY target \"result\"\
+\n with command \"command\" and dependencies \"dependencies\". Note that\
+\n _-extra-phony foo bar \"\"_ is a regular way to add the target \"bar\" as\
+\n as a dependencies of an already defined target \"foo\".\
+\n[-I dir]: look for Objective Caml dependencies in \"dir\"\
+\n[-R physicalpath logicalpath]: look for Coq dependencies resursively\
+\n  starting from \"physicalpath\". The logical path associated to the\
+\n  physical path is \"logicalpath\".\
+\n[-Q physicalpath logicalpath]: look for Coq dependencies starting from\
+\n  \"physicalpath\". The logical path associated to the physical path\
+\n  is \"logicalpath\".\
+\n[VARIABLE = value]: Add the variable definition \"VARIABLE=value\"\
+\n[-byte]: compile with byte-code version of coq\
+\n[-opt]: compile with native-code version of coq\
+\n[-arg opt]: send option \"opt\" to coqc\
+\n[-install opt]: where opt is \"user\" to force install into user directory,\
+\n  \"none\" to build a makefile with no install target or\
+\n  \"global\" to force install in $COQLIB directory\
+\n[-f file]: take the contents of file as arguments\
+\n[-o file]: output should go in file file\
+\n	Output file outside the current directory is forbidden.\
+\n[-h]: print this usage summary\
+\n[--help]: equivalent to [-h]\n";
   exit 1
 
 let is_genrule r = (* generic rule (like bar%foo: ...) *)
@@ -264,8 +264,8 @@ let where_put_doc = function
       then
 	physical_dir_of_logical_dir pr
       else
-	let () = prerr_string "Warning: -Q options don't have a correct common prefix,
- install-doc will put anything in $INSTALLDEFAULTROOT\n" in
+	let () = prerr_string ("Warning: -Q options don't have a correct common prefix,"
+                        ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in
 	"$(INSTALLDEFAULTROOT)"
     |_,inc_i,((_,lp,_)::q as inc_r) ->
       let pr = List.fold_left (fun a (_,b,_) -> string_prefix a b) lp q in
@@ -277,8 +277,8 @@ let where_put_doc = function
       then
 	physical_dir_of_logical_dir pr
       else
-	let () = prerr_string "Warning: -R/-Q options don't have a correct common prefix,
- install-doc will put anything in $INSTALLDEFAULTROOT\n" in
+	let () = prerr_string ("Warning: -R/-Q options don't have a correct common prefix,"
+                        ^ " install-doc will put anything in $INSTALLDEFAULTROOT\n") in
 	"$(INSTALLDEFAULTROOT)"
 
 let install (vfiles,(mlis,ml4s,mls,mllibs,mlpacks),_,sds) inc = function
@@ -518,8 +518,8 @@ let variables is_install opt (args,defs) =
     if !some_ml4file || !some_mlfile || !some_mlifile then begin
     print "COQSRCLIBS?=" ;
     List.iter (fun c -> print "-I \"$(COQLIB)"; print c ; print "\" \\\n") lib_dirs ;
-    List.iter (fun c -> print " \\
-  -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
+    List.iter (fun c -> print " \\\
+\n  -I \"$(COQLIB)/"; print c; print "\"") Coq_config.plugins_dirs; print "\n";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n\n";
     print "CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread -safe-string\n";
     print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread -safe-string\n";
@@ -529,8 +529,8 @@ let variables is_install opt (args,defs) =
     print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n";
     print "GRAMMARS?=grammar.cma\n";
     print "CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo\n";
-    print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\
-  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
+    print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \\\
+\n  $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
     end;
     match is_install with
       | Project_file.NoInstall -> ()
@@ -816,14 +816,14 @@ let all_target (vfiles, (_,_,_,_,mlpackfiles as mlfiles), sps, sds) inc =
 
 let banner () =
   print (Printf.sprintf
-"#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \\VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V%s ##
-#############################################################################
-
-" (Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
+"#############################################################################\
+\n##  v      #                   The Coq Proof Assistant                     ##\
+\n## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##\
+\n##   \\VV/  #                                                               ##\
+\n##    //   #  Makefile automagically generated by coq_makefile V%s ##\
+\n#############################################################################\
+\n\n"
+(Coq_config.version ^ String.make (10 - String.length Coq_config.version) ' '))
 
 let warning () =
   print "# WARNING\n#\n";
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 66f782ffbe..e457ca61d0 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -83,7 +83,7 @@ let print_usage_channel co command =
 \n  -m, --memory           display total heap size at program exit\
 \n                         (use environment variable\
 \n                          OCAML_GC_STATS=\"/tmp/gclog.txt\"\
-\n                          for full Gc stats dump)
+\n                          for full Gc stats dump)\
 \n  -native-compiler       precompile files for the native_compute machinery\
 \n  -h, -help, --help      print this list of options\
 \n";
-- 
cgit v1.2.3