Delete trailing whitespaces in all *.{v,ml*} files

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

1 files changed, 74 insertions, 74 deletions

diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 3c4c9a6566..d2b66f9939 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -54,7 +54,7 @@ let usage () =
   prerr_endline "  --files-from <file>  read file names to process in <file>";
   prerr_endline "  --glob-from <file>   read globalization information from <file>";
   prerr_endline "  --quiet              quiet mode (default)";
-  prerr_endline "  --verbose            verbose mode";  
+  prerr_endline "  --verbose            verbose mode";
   prerr_endline "  --no-externals       no links to Coq standard library";
   prerr_endline "  --coqlib <url>       set URL for Coq standard library";
   prerr_endline ("                       (default is " ^ Coq_config.wwwstdlib ^ ")");
@@ -80,20 +80,20 @@ let obsolete s =
 
 (*s \textbf{Banner.} Always printed. Notice that it is printed on error
     output, so that when the output of [coqdoc] is redirected this header
-    is not (unless both standard and error outputs are redirected, of 
+    is not (unless both standard and error outputs are redirected, of
     course). *)
 
 let banner () =
   eprintf "This is coqdoc version %s, compiled on %s\n"
     Coq_config.version Coq_config.compile_date;
   flush stderr
-    
-let target_full_name f = 
+
+let target_full_name f =
   match !Cdglobals.target_language with
     | HTML -> f ^ ".html"
     | Raw -> f ^ ".txt"
     | _ -> f ^ ".tex"
-	
+
 (*s \textbf{Separation of files.} Files given on the command line are
     separated according to their type, which is determined by their
     suffix.  Coq files have suffixe \verb!.v! or \verb!.g! and \LaTeX\
@@ -106,7 +106,7 @@ let check_if_file_exists f =
   end
 
 
-(*s Manipulations of paths and path aliases *) 
+(*s Manipulations of paths and path aliases *)
 
 let normalize_path p =
   (* We use the Unix subsystem to normalize a physical path (relative
@@ -117,7 +117,7 @@ let normalize_path p =
   let orig = Sys.getcwd () in
     Sys.chdir p;
     let res = Sys.getcwd () in
-      Sys.chdir orig; 
+      Sys.chdir orig;
       res
 
 let normalize_filename f =
@@ -127,22 +127,22 @@ let normalize_filename f =
 
 (* [paths] maps a physical path to a name *)
 let paths = ref []
-  
-let add_path dir name = 
+
+let add_path dir name =
   (* if dir is relative we add both the relative and absolute name *)
   let p = normalize_path dir in
     paths := (p,name) :: !paths
-  
+
 (* turn A/B/C into A.B.C *)
 let name_of_path = Str.global_replace (Str.regexp "/") ".";;
 
-let coq_module filename = 
+let coq_module filename =
   let bfname = Filename.chop_extension filename in
   let nfname = normalize_filename bfname in
-  let rec change_prefix map f = 
+  let rec change_prefix map f =
     match map with
-      | [] -> 
-	  (* There is no prefix alias; 
+      | [] ->
+	  (* There is no prefix alias;
 	     we just cut the name wrt current working directory *)
 	  let cwd = Sys.getcwd () in
 	  let exp = Str.regexp (Str.quote (cwd ^ "/")) in
@@ -166,10 +166,10 @@ let what_file f =
     Vernac_file (f, coq_module f)
   else if Filename.check_suffix f ".tex" then
     Latex_file f
-  else 
+  else
      (eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1)
-    
-(*s \textbf{Reading file names from a file.} 
+
+(*s \textbf{Reading file names from a file.}
  *  File names may be given
  *  in a file instead of being given on the command
  *  line. [(files_from_file f)] returns the list of file names contained
@@ -187,7 +187,7 @@ let files_from_file f =
 	    | ' ' | '\t' | '\n' ->
 		if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
 		Buffer.clear buf
-	    | c -> 
+	    | c ->
 		Buffer.add_char buf c
 	done; []
       with End_of_file ->
@@ -202,9 +202,9 @@ let files_from_file f =
       eprintf "\ncoqdoc: cannot read from file %s (%s)\n" f s;
       exit 1
     end
-      
+
 (*s \textbf{Parsing of the command line.} *)
-      
+
 let dvi = ref false
 let ps = ref false
 let pdf = ref false
@@ -214,7 +214,7 @@ let parse () =
   let add_file f = files := f :: !files in
   let rec parse_rec = function
     | [] -> ()
-	
+
     | ("-nopreamble" | "--nopreamble" | "--no-preamble"
       |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
 	header_trailer := false; parse_rec rem
@@ -244,11 +244,11 @@ let parse () =
 	out_to := StdOut; parse_rec rem
     | ("-o" | "--output") :: f :: rem ->
 	out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
-    | ("-o" | "--output") :: [] -> 
+    | ("-o" | "--output") :: [] ->
 	usage ()
     | ("-d" | "--directory") :: dir :: rem ->
 	output_dir := dir; parse_rec rem
-    | ("-d" | "--directory") :: [] -> 
+    | ("-d" | "--directory") :: [] ->
 	usage ()
     | ("-s" | "--short") :: rem ->
 	short := true; parse_rec rem
@@ -293,8 +293,8 @@ let parse () =
     | ("-toc-depth" | "--toc-depth") :: [] ->
       usage ()
     | ("-toc-depth" | "--toc-depth") :: ds :: rem ->
-      let d = try int_of_string ds with 
-                Failure _ -> 
+      let d = try int_of_string ds with
+                Failure _ ->
                   (eprintf "--toc-depth must be followed by an integer";
                    exit 1)
       in
@@ -314,32 +314,32 @@ let parse () =
 	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
 	Cdglobals.set_utf8 (); parse_rec rem
-	  
+
     | ("-q" | "-quiet" | "--quiet") :: rem ->
 	quiet := true; parse_rec rem
     | ("-v" | "-verbose" | "--verbose") :: rem ->
 	quiet := false; parse_rec rem
-	  
+
     | ("-h" | "-help" | "-?" | "--help") :: rem ->
 	banner (); usage ()
     | ("-V" | "-version" | "--version") :: _ ->
 	banner (); exit 0
 
-    | ("-vernac-file" | "--vernac-file") :: f :: rem -> 
+    | ("-vernac-file" | "--vernac-file") :: f :: rem ->
 	check_if_file_exists f;
 	add_file (Vernac_file (f, coq_module f)); parse_rec rem
     | ("-vernac-file" | "--vernac-file") :: [] ->
 	usage ()
-    | ("-tex-file" | "--tex-file") :: f :: rem -> 
+    | ("-tex-file" | "--tex-file") :: f :: rem ->
 	add_file (Latex_file f); parse_rec rem
     | ("-tex-file" | "--tex-file") :: [] ->
 	usage ()
     | ("-files" | "--files" | "--files-from") :: f :: rem ->
-	List.iter (fun f -> add_file (what_file f)) (files_from_file f); 
+	List.iter (fun f -> add_file (what_file f)) (files_from_file f);
 	parse_rec rem
     | ("-files" | "--files") :: [] ->
 	usage ()
-    | "-R" :: path :: log :: rem -> 
+    | "-R" :: path :: log :: rem ->
 	add_path path log; parse_rec rem
     | "-R" :: ([] | [_]) ->
 	usage ()
@@ -359,16 +359,16 @@ let parse () =
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->
 	usage ()
-    | f :: rem -> 
+    | f :: rem ->
 	add_file (what_file f); parse_rec rem
-  in 
+  in
     parse_rec (List.tl (Array.to_list Sys.argv));
     Output.initialize ();
     List.rev !files
 
-      
+
 (*s The following function produces the output. The default output is
-    the \LaTeX\ document: in that case, we just call [Web.produce_document]. 
+    the \LaTeX\ document: in that case, we just call [Web.produce_document].
     If option \verb!-dvi!, \verb!-ps! or \verb!-html! is invoked, then
     we make calls to \verb!latex! or \verb!dvips! or \verb!pdflatex! accordingly. *)
 
@@ -390,9 +390,9 @@ let clean_temp_files basefile =
     remove (basefile ^ ".pdf");
     remove (basefile ^ ".haux");
     remove (basefile ^ ".html")
-      
+
 let clean_and_exit file res = clean_temp_files file; exit res
-  
+
 let cat file =
   let c = open_in file in
     try
@@ -401,7 +401,7 @@ let cat file =
       close_in c
 
 let copy src dst =
-  let cin = open_in src 
+  let cin = open_in src
   and cout = open_out dst in
     try
       while true do Pervasives.output_char cout (input_char cin) done
@@ -413,7 +413,7 @@ let copy src dst =
 
 let gen_one_file l =
   let file = function
-    | Vernac_file (f,m) -> 
+    | Vernac_file (f,m) ->
         let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
           Output.set_module m sub;
           Cpretty.coq_file f m
@@ -424,57 +424,57 @@ let gen_one_file l =
     List.iter file l;
     if !index then Output.make_index();
     if (!header_trailer) then Output.trailer ()
-      
+
 let gen_mult_files l =
   let file = function
-    | Vernac_file (f,m) -> 
+    | Vernac_file (f,m) ->
       let sub = if !lib_subtitles then Cpretty.detect_subtitle f m else None in
 	let hf = target_full_name m in
         Output.set_module m sub;
 	  open_out_file hf;
-	  if (!header_trailer) then Output.header (); 
-	  Cpretty.coq_file f m; 
+	  if (!header_trailer) then Output.header ();
+	  Cpretty.coq_file f m;
 	  if (!header_trailer) then Output.trailer ();
 	  close_out_file()
     | Latex_file _ -> ()
   in
     List.iter file l;
     if (!index && !target_language=HTML) then begin
-      if (!multi_index) then Output.make_multi_index (); 
-      open_out_file (!index_name^".html"); 
+      if (!multi_index) then Output.make_multi_index ();
+      open_out_file (!index_name^".html");
       page_title := (if !title <> "" then !title else "Index");
-      if (!header_trailer) then Output.header (); 
-      Output.make_index (); 
+      if (!header_trailer) then Output.header ();
+      Output.make_index ();
       if (!header_trailer) then Output.trailer ();
       close_out_file()
     end;
     if (!toc && !target_language=HTML) then begin
-      open_out_file "toc.html"; 
+      open_out_file "toc.html";
       page_title := (if !title <> "" then !title else "Table of contents");
       if (!header_trailer) then Output.header ();
       if !title <> "" then printf "<h1>%s</h1>\n" !title;
-      Output.make_toc (); 
+      Output.make_toc ();
       if (!header_trailer) then Output.trailer ();
       close_out_file()
-    end 
+    end
       (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
 
 let read_glob x =
   match x with
-    | Vernac_file (f,m) ->   
+    | Vernac_file (f,m) ->
 	let glob = (Filename.chop_extension f) ^ ".glob" in
  	  (try
 	      Vernac_file (f, Index.read_glob glob)
-            with e -> 
+            with e ->
               eprintf "Warning: file %s cannot be used; links will not be available: %s\n" glob (Printexc.to_string e);
 	      x)
   | Latex_file _ -> x
 
 let index_module = function
-  | Vernac_file (f,m) ->   
+  | Vernac_file (f,m) ->
       Index.add_module m
   | Latex_file _ -> ()
-      
+
 let produce_document l =
   (if !target_language=HTML then
     let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in
@@ -482,8 +482,8 @@ let produce_document l =
       if (Sys.file_exists src) then (copy src dst) else eprintf "Warning: file %s does not exist\n" src);
   (if !target_language=LaTeX then
       let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
-      let dst = if !output_dir <> "" then 
-	  Filename.concat !output_dir "coqdoc.sty" 
+      let dst = if !output_dir <> "" then
+	  Filename.concat !output_dir "coqdoc.sty"
 	else "coqdoc.sty" in
 	if Sys.file_exists src then copy src dst else eprintf "Warning: file %s does not exist\n" src);
   (match !Cdglobals.glob_source with
@@ -492,7 +492,7 @@ let produce_document l =
     | GlobFile f -> ignore (Index.read_glob f));
   List.iter index_module l;
   match !out_to with
-    | StdOut -> 
+    | StdOut ->
 	Cdglobals.out_channel := stdout;
 	gen_one_file l
     | File f ->
@@ -501,11 +501,11 @@ let produce_document l =
 	close_out_file()
     | MultFiles ->
 	gen_mult_files l
-	  
+
 let produce_output fl =
-  if not (!dvi || !ps || !pdf) then 
+  if not (!dvi || !ps || !pdf) then
     produce_document fl
-  else 
+  else
     begin
       let texfile = Filename.temp_file "coqdoc" ".tex" in
       let basefile = Filename.chop_suffix texfile ".tex" in
@@ -513,52 +513,52 @@ let produce_output fl =
 	out_to := File texfile;
 	output_dir := (Filename.dirname texfile);
 	produce_document fl;
-	
+
 	let latexexe = if !pdf then "pdflatex" else "latex" in
-	let latexcmd = 
+	let latexcmd =
 	  let file = Filename.basename texfile in
-	  let file = 
-	    if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+	  let file =
+	    if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file
 	  in
 	    sprintf "%s %s && %s %s 1>&2 %s" latexexe file latexexe file (if !quiet then "> /dev/null" else "")
 	in
 	let res = locally (Filename.dirname texfile) Sys.command latexcmd in
 	  if res <> 0 then begin
-	      eprintf "Couldn't run LaTeX successfully\n"; 
+	      eprintf "Couldn't run LaTeX successfully\n";
 	      clean_and_exit basefile res
 	    end;
-	  
+
 	  let dvifile = basefile ^ ".dvi" in
-	    if !dvi then 
+	    if !dvi then
 	      begin
 		match final_out_to with
 		  | MultFiles | StdOut -> cat dvifile
 		  | File f -> copy dvifile f
 	      end;
 	  let pdffile = basefile ^ ".pdf" in
-	    if !pdf then 
+	    if !pdf then
             begin
 	        match final_out_to with
 		  | MultFiles | StdOut -> cat pdffile
 		  | File f -> copy pdffile f
 	    end;
 	    if !ps then begin
-	        let psfile = basefile ^ ".ps" 
+	        let psfile = basefile ^ ".ps"
 		in
-		let command = 
-		  sprintf "dvips %s -o %s %s" dvifile psfile 
+		let command =
+		  sprintf "dvips %s -o %s %s" dvifile psfile
 		    (if !quiet then "> /dev/null 2>&1" else "")
 		in
 		let res = Sys.command command in
 		  if res <> 0 then begin
-		      eprintf "Couldn't run dvips successfully\n"; 
+		      eprintf "Couldn't run dvips successfully\n";
 		      clean_and_exit basefile res
 		    end;
 		  match final_out_to with
 		    | MultFiles | StdOut -> cat psfile
 		    | File f -> copy psfile f
 	      end;
-	 
+
 	    clean_temp_files basefile
     end
 
@@ -570,5 +570,5 @@ let main () =
   let files = parse () in
     if not !quiet then banner ();
     if files <> [] then produce_output files
-      
+
 let _ = Printexc.catch main ()