[coq] Untabify the whole ML codebase.

We also remove trailing whitespace.

Script used:

```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```

10 files changed, 447 insertions, 447 deletions

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index b091ff3b4e..f8f046ae75 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -181,7 +181,7 @@ let generate_conf_subdirs oc sds =
   iter (fprintf oc "clean::\n\tcd \"%s\" && $(MAKE) clean\n") sds;
   iter (fprintf oc "archclean::\n\tcd \"%s\" && $(MAKE) archclean\n") sds;
   iter (fprintf oc "install-extra::\n\tcd \"%s\" && $(MAKE) install\n") sds
-   
+
 
 let generate_conf_includes oc { ml_includes; r_includes; q_includes } =
   section oc "Path directives (-I, -R, -Q).";
@@ -307,7 +307,7 @@ let ensure_root_dir
         r_includes = source (here_path, "Top") :: r_includes }
 ;;
 
-let warn_install_at_root_directory 
+let warn_install_at_root_directory
   ({ q_includes; r_includes; } as project)
 =
   let open CList in
@@ -330,11 +330,11 @@ let check_overlapping_include { q_includes; r_includes } =
   let aux = function
     | [] -> ()
     | {thing = { path; canonical_path }, _} :: l ->
-	if not (is_prefix pwd canonical_path) then
-	  eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path;
+        if not (is_prefix pwd canonical_path) then
+          eprintf "Warning: %s (used in -R or -Q) is not a subdirectory of the current directory\n\n" path;
         List.iter (fun {thing={ path = p; canonical_path = cp }, _} ->
-	  if is_prefix canonical_path cp  || is_prefix cp canonical_path then
-	    eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n"
+          if is_prefix canonical_path cp  || is_prefix cp canonical_path then
+            eprintf "Warning: %s and %s overlap (used in -R or -Q)\n\n"
               path p) l
   in
     aux (q_includes @ r_includes)
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 371483b862..8077f166c8 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -118,9 +118,9 @@ let insert texfile coq_output result =
     let rec read_lines () =
       let s = input_line c_coq in
       if Str.string_match any_prompt s 0 then begin
-	last_read := s; []
+        last_read := s; []
       end else
-	s :: read_lines () in
+        s :: read_lines () in
     (first :: read_lines (), !nb) in
   let unhandled_output = ref None in
   let read_output () =
@@ -225,7 +225,7 @@ let one_file texfile =
     extract texfile inputv;
     (* 2. run Coq on input *)
     let _ = Sys.command (Printf.sprintf "%s < %s > %s 2>&1" !image inputv
-			   coq_output)
+                           coq_output)
     in
     (* 3. insert Coq output into original file *)
     insert texfile coq_output result;
@@ -244,21 +244,21 @@ let files = ref []
 let parse_cl () =
   Arg.parse
       [ "-o", Arg.String (fun s -> output_specified := true; output := s),
-	"output-file    Specify the resulting LaTeX file";
-	"-n", Arg.Int (fun n -> linelen := n),
-	"line-width     Set the line width";
-	"-image", Arg.String (fun s -> image := s),
-	"coq-image  Use coq-image as Coq command";
-	"-w", Arg.Set cut_at_blanks,
-	"               Try to cut lines at blanks";
-	"-v", Arg.Set verbose,
-	"               Verbose mode (show Coq answers on stdout)";
-	"-sl", Arg.Set slanted,
-	"              Coq answers in slanted font (only with LaTeX2e)";
-	"-hrule", Arg.Set hrule,
-	"           Coq parts are written between 2 horizontal lines";
-	"-small", Arg.Set small,
-	"           Coq parts are written in small font";
+        "output-file    Specify the resulting LaTeX file";
+        "-n", Arg.Int (fun n -> linelen := n),
+        "line-width     Set the line width";
+        "-image", Arg.String (fun s -> image := s),
+        "coq-image  Use coq-image as Coq command";
+        "-w", Arg.Set cut_at_blanks,
+        "               Try to cut lines at blanks";
+        "-v", Arg.Set verbose,
+        "               Verbose mode (show Coq answers on stdout)";
+        "-sl", Arg.Set slanted,
+        "              Coq answers in slanted font (only with LaTeX2e)";
+        "-hrule", Arg.Set hrule,
+        "           Coq parts are written between 2 horizontal lines";
+        "-small", Arg.Set small,
+        "           Coq parts are written in small font";
       ]
       (fun s -> files := s :: !files)
       "coq-tex [options] file ..."
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index b9a8601d10..0528d73713 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -41,7 +41,7 @@ let warning_mult suf iter =
       if (Filename.dirname (file_name f d))
         <> (Filename.dirname (file_name f d')) then begin
           coqdep_warning "the file %s is defined twice!" (f ^ suf)
-	end
+        end
     with Not_found -> () end;
     Hashtbl.add tab f d
   in
@@ -56,20 +56,20 @@ let sort () =
       let cin = open_in (file ^ ".v") in
       let lb = Lexing.from_channel cin in
       try
-	while true do
-	  match coq_action lb with
-	    | Require (from, sl) ->
-		List.iter
-		  (fun s ->
+        while true do
+          match coq_action lb with
+            | Require (from, sl) ->
+                List.iter
+                  (fun s ->
                     match search_v_known ?from s with
                     | None -> ()
                     | Some f -> loop f)
-		sl
-	    | _ -> ()
-	done
+                sl
+            | _ -> ()
+        done
       with Fin_fichier ->
-	close_in cin;
-	printf "%s%s " file !suffixe
+        close_in cin;
+        printf "%s%s " file !suffixe
     end
   in
   List.iter (fun (name,_) -> loop name) !vAccu
@@ -85,18 +85,18 @@ let mL_dep_list b f =
       let chan = open_in f in
       let buf = Lexing.from_channel chan in
       try
-	while true do
-	  let (Use_module str) = caml_action buf in
-	  if str = b then begin
+        while true do
+          let (Use_module str) = caml_action buf in
+          if str = b then begin
             coqdep_warning "in file %s the notation %s. is useless !\n" f b
-	  end else
+          end else
             if not (List.mem str !deja_vu) then addQueue deja_vu str
-      	done; []
+        done; []
       with Fin_fichier -> begin
-	close_in chan;
-	let rl = List.rev !deja_vu in
-      	Hashtbl.add dep_tab f rl;
-	rl
+        close_in chan;
+        let rl = List.rev !deja_vu in
+        Hashtbl.add dep_tab f rl;
+        rl
       end
     with Sys_error _ -> []
 
@@ -116,36 +116,36 @@ let traite_Declare f =
   let decl_list = ref ([] : string list) in
   let rec treat = function
     | s :: ll ->
-	let s' = basename_noext s in
-	(match search_ml_known s with
-	   | Some mldir when not (List.mem s' !decl_list) ->
-	       let fullname = file_name s' mldir in
-	       let depl = mL_dep_list s (fullname ^ ".ml") in
-	       treat depl;
-	       decl_list := s :: !decl_list
-	   | _ -> ());
-	treat ll
+        let s' = basename_noext s in
+        (match search_ml_known s with
+           | Some mldir when not (List.mem s' !decl_list) ->
+               let fullname = file_name s' mldir in
+               let depl = mL_dep_list s (fullname ^ ".ml") in
+               treat depl;
+               decl_list := s :: !decl_list
+           | _ -> ());
+        treat ll
     | [] -> ()
   in
     try
       let chan = open_in f in
       let buf = Lexing.from_channel chan in
-	begin try
-	    while true do
-      	      let tok = coq_action buf in
-      		(match tok with
-		  | Declare sl ->
-		      decl_list := [];
-		      treat sl;
-		      decl_list := List.rev !decl_list;
-		      if !option_D then
-			affiche_Declare f !decl_list
-		      else if !decl_list <> sl then
-			warning_Declare f !decl_list
-		  | _ -> ())
-	    done
-	  with Fin_fichier -> () end;
-	close_in chan
+        begin try
+            while true do
+              let tok = coq_action buf in
+                (match tok with
+                  | Declare sl ->
+                      decl_list := [];
+                      treat sl;
+                      decl_list := List.rev !decl_list;
+                      if !option_D then
+                        affiche_Declare f !decl_list
+                      else if !decl_list <> sl then
+                        warning_Declare f !decl_list
+                  | _ -> ())
+            done
+          with Fin_fichier -> () end;
+        close_in chan
     with Sys_error _ -> ()
 
 let declare_dependencies () =
@@ -246,7 +246,7 @@ struct
       else
         let x = NSet.choose rem in
         let rem = NSet.remove x rem in
-        if NSet.mem x seen then 
+        if NSet.mem x seen then
           aux rem seen
         else
           let seen = NSet.add x seen in
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index c5f38e716e..775c528176 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -631,13 +631,13 @@ let rec treat_file old_dirname old_name =
            Array.iter (treat_file (Some newdirname)) (Sys.readdir complete_name))
     | S_REG ->
         (match get_extension name [".v";".ml";".mli";".mlg";".mllib";".mlpack"] with
-	   | (base,".v") ->
-	       let name = file_name base dirname
-	       and absname = absolute_file_name base dirname in
-	       addQueue vAccu (name, absname)
+           | (base,".v") ->
+               let name = file_name base dirname
+               and absname = absolute_file_name base dirname in
+               addQueue vAccu (name, absname)
            | (base,(".ml"|".mlg" as ext)) -> addQueue mlAccu (base,ext,dirname)
-	   | (base,".mli") -> addQueue mliAccu (base,dirname)
-	   | (base,".mllib") -> addQueue mllibAccu (base,dirname)
-	   | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
-	   | _ -> ())
+           | (base,".mli") -> addQueue mliAccu (base,dirname)
+           | (base,".mllib") -> addQueue mllibAccu (base,dirname)
+           | (base,".mlpack") -> addQueue mlpackAccu (base,dirname)
+           | _ -> ())
     | _ -> ()
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 8f82bee5c6..67a835957d 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -133,8 +133,8 @@ type 'a index = {
 let map f i =
   { i with idx_entries =
       List.map
-	(fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l))
-	i.idx_entries }
+        (fun (c,l) -> (c, List.map (fun (s,x) -> (s,f s x)) l))
+        i.idx_entries }
 
 let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2
 
@@ -148,7 +148,7 @@ let sort_entries el =
     (fun ((s,_) as e) ->
       let c = Alpha.norm_char s.[0] in
       let c,l =
-	try c,Hashtbl.find t c with Not_found -> '*',Hashtbl.find t '*' in
+        try c,Hashtbl.find t c with Not_found -> '*',Hashtbl.find t '*' in
       Hashtbl.replace t c (e :: l))
     el;
   let res = ref [] in
@@ -208,22 +208,22 @@ let prepare_entry s = function
       let quoted = ref false in
       let l = String.length s - 1 in
       while !j <= l do
-	if not !quoted then begin
-	  (match s.[!j] with
-	  | '_' -> Bytes.set ntn !k ' '; incr k
-	  | 'x' -> Bytes.set ntn !k '_'; incr k
-	  | '\'' -> quoted := true
-	  | _ -> assert false)
-	end
-	else
-	  if s.[!j] = '\'' then
-	    if (!j = l || s.[!j+1] = '_') then quoted := false
-	    else (incr j; Bytes.set ntn !k s.[!j]; incr k)
-	  else begin
-	    Bytes.set ntn !k s.[!j];
-	    incr k
-	  end;
-	incr j
+        if not !quoted then begin
+          (match s.[!j] with
+          | '_' -> Bytes.set ntn !k ' '; incr k
+          | 'x' -> Bytes.set ntn !k '_'; incr k
+          | '\'' -> quoted := true
+          | _ -> assert false)
+        end
+        else
+          if s.[!j] = '\'' then
+            if (!j = l || s.[!j+1] = '_') then quoted := false
+            else (incr j; Bytes.set ntn !k s.[!j]; incr k)
+          else begin
+            Bytes.set ntn !k s.[!j];
+            incr k
+          end;
+        incr j
       done;
       let ntn = Bytes.sub_string ntn 0 !k in
       let ntn = if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" in
@@ -246,8 +246,8 @@ let all_entries () =
       idx_entries = sort_entries !gl;
       idx_size = List.length !gl },
     Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t;
-			             idx_entries = sort_entries e;
-			             idx_size = List.length e }) :: l) bt []
+                                     idx_entries = sort_entries e;
+                                     idx_size = List.length e }) :: l) bt []
 
 let type_of_string = function
   | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
@@ -297,16 +297,16 @@ let read_glob vfile f =
       let s = input_line c in
       let n = String.length s in
       if n > 0 then begin
-	match s.[0] with
-	  | 'F' ->
-	      cur_mod := String.sub s 1 (n - 1);
-	      current_library := !cur_mod
-	  | 'R' ->
-	      (try
-		Scanf.sscanf s "R%d:%d %s %s %s %s"
-		  (fun loc1 loc2 lib_dp sp id ty ->
-		    for loc=loc1 to loc2 do
-		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty);
+        match s.[0] with
+          | 'F' ->
+              cur_mod := String.sub s 1 (n - 1);
+              current_library := !cur_mod
+          | 'R' ->
+              (try
+                Scanf.sscanf s "R%d:%d %s %s %s %s"
+                  (fun loc1 loc2 lib_dp sp id ty ->
+                    for loc=loc1 to loc2 do
+                      add_ref !cur_mod loc lib_dp sp id (type_of_string ty);
 
                       (* Also add an entry for each module mentioned in [lib_dp],
                        * to use in interpolation. *)
@@ -316,13 +316,13 @@ let read_glob vfile f =
                                                                 | _ -> thisPiece ^ "." ^ priorPieces in
                                                 add_ref !cur_mod loc "" "" newPieces Library;
                                                 newPieces) (Str.split (Str.regexp_string ".") lib_dp) "")
-		    done)
-	       with _ -> ())
-	  | _ ->
-	      try Scanf.sscanf s "%s %d:%d %s %s"
-		(fun ty loc1 loc2 sp id ->
+                    done)
+               with _ -> ())
+          | _ ->
+              try Scanf.sscanf s "%s %d:%d %s %s"
+                (fun ty loc1 loc2 sp id ->
                   add_def loc1 loc2 (type_of_string ty) sp id)
-	      with Scanf.Scan_failure _ -> ()
+              with Scanf.Scan_failure _ -> ()
 
       end
     done; assert false
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 3442ebb731..529706f153 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -132,8 +132,8 @@ let coq_module filename =
     (* otherwise, keep only base name *)
     | [] -> fname
     | (p, name) :: rem ->
-	try name_of_path p name dirname [fname]
-	with Not_found -> change_prefix rem
+        try name_of_path p name dirname [fname]
+        with Not_found -> change_prefix rem
   in
   change_prefix !paths
 
@@ -159,22 +159,22 @@ let files_from_file f =
     let buf = Buffer.create 80 in
     let l = ref [] in
       try
-	while true do
-	  match input_char ch with
-	    | ' ' | '\t' | '\n' ->
-		if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
-		Buffer.clear buf
-	    | c ->
-		Buffer.add_char buf c
-	done; []
+        while true do
+          match input_char ch with
+            | ' ' | '\t' | '\n' ->
+                if Buffer.length buf > 0 then l := (Buffer.contents buf) :: !l;
+                Buffer.clear buf
+            | c ->
+                Buffer.add_char buf c
+        done; []
       with End_of_file ->
-	List.rev !l
+        List.rev !l
   in
     try
       check_if_file_exists f;
       let ch = open_in f in
       let l = files_from_channel ch in
-	close_in ch;l
+        close_in ch;l
     with Sys_error s -> begin
       eprintf "coqdoc: cannot read from file %s (%s)\n" f s;
       exit 1
@@ -194,79 +194,79 @@ let parse () =
 
     | ("-nopreamble" | "--nopreamble" | "--no-preamble"
       |  "-bodyonly"   | "--bodyonly"   | "--body-only") :: rem ->
-	header_trailer := false; parse_rec rem
+        header_trailer := false; parse_rec rem
     | ("-with-header" | "--with-header") :: f ::rem ->
-	header_trailer := true; header_file_spec := true; header_file := f; parse_rec rem
+        header_trailer := true; header_file_spec := true; header_file := f; parse_rec rem
     | ("-with-header" | "--with-header") :: [] ->
-	usage ()
+        usage ()
     | ("-with-footer" | "--with-footer") :: f ::rem ->
-	header_trailer := true; footer_file_spec := true; footer_file := f; parse_rec rem
+        header_trailer := true; footer_file_spec := true; footer_file := f; parse_rec rem
     | ("-with-footer" | "--with-footer") :: [] ->
-	usage ()
+        usage ()
     | ("-p" | "--preamble") :: s :: rem ->
-	Output.push_in_preamble s; parse_rec rem
+        Output.push_in_preamble s; parse_rec rem
     | ("-p" | "--preamble") :: [] ->
-	usage ()
+        usage ()
     | ("-noindex" | "--noindex" | "--no-index") :: rem ->
-	index := false; parse_rec rem
+        index := false; parse_rec rem
     | ("-multi-index" | "--multi-index") :: rem ->
-	multi_index := true; parse_rec rem
+        multi_index := true; parse_rec rem
     | ("-index" | "--index") :: s :: rem ->
-	Cdglobals.index_name := s; parse_rec rem
+        Cdglobals.index_name := s; parse_rec rem
     | ("-index" | "--index") :: [] ->
-	usage ()
+        usage ()
     | ("-toc" | "--toc" | "--table-of-contents") :: rem ->
-	toc := true; parse_rec rem
+        toc := true; parse_rec rem
     | ("-stdout" | "--stdout") :: rem ->
-	out_to := StdOut; parse_rec rem
+        out_to := StdOut; parse_rec rem
     | ("-o" | "--output") :: f :: rem ->
-	out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
+        out_to := File (Filename.basename f); output_dir := Filename.dirname f; parse_rec rem
     | ("-o" | "--output") :: [] ->
-	usage ()
+        usage ()
     | ("-d" | "--directory") :: dir :: rem ->
-	output_dir := dir; parse_rec rem
+        output_dir := dir; parse_rec rem
     | ("-d" | "--directory") :: [] ->
-	usage ()
+        usage ()
     | ("-s" | "--short") :: rem ->
-	short := true; parse_rec rem
+        short := true; parse_rec rem
     | ("-l" | "-light" | "--light") :: rem ->
-	gallina := true; light := true; parse_rec rem
+        gallina := true; light := true; parse_rec rem
     | ("-g" | "-gallina" | "--gallina") :: rem ->
-	gallina := true; parse_rec rem
+        gallina := true; parse_rec rem
     | ("-t" | "-title" | "--title") :: s :: rem ->
-	title := s; parse_rec rem
+        title := s; parse_rec rem
     | ("-t" | "-title" | "--title") :: [] ->
-	usage ()
+        usage ()
     | ("-latex" | "--latex") :: rem ->
-	Cdglobals.target_language := LaTeX; parse_rec rem
+        Cdglobals.target_language := LaTeX; parse_rec rem
     | ("-pdf" | "--pdf") :: rem ->
-	Cdglobals.target_language := LaTeX; pdf := true; parse_rec rem
+        Cdglobals.target_language := LaTeX; pdf := true; parse_rec rem
     | ("-dvi" | "--dvi") :: rem ->
-	Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem
+        Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem
     | ("-ps" | "--ps") :: rem ->
-	Cdglobals.target_language := LaTeX; ps := true; parse_rec rem
+        Cdglobals.target_language := LaTeX; ps := true; parse_rec rem
     | ("-html" | "--html") :: rem ->
-	Cdglobals.target_language := HTML; parse_rec rem
+        Cdglobals.target_language := HTML; parse_rec rem
     | ("-texmacs" | "--texmacs") :: rem ->
-	Cdglobals.target_language := TeXmacs; parse_rec rem
+        Cdglobals.target_language := TeXmacs; parse_rec rem
     | ("-raw" | "--raw") :: rem ->
-	Cdglobals.target_language := Raw; parse_rec rem
+        Cdglobals.target_language := Raw; parse_rec rem
     | ("-charset" | "--charset") :: s :: rem ->
-	Cdglobals.charset := s; parse_rec rem
+        Cdglobals.charset := s; parse_rec rem
     | ("-charset" | "--charset") :: [] ->
-	usage ()
+        usage ()
     | ("-inputenc" | "--inputenc") :: s :: rem ->
-	Cdglobals.inputenc := s; parse_rec rem
+        Cdglobals.inputenc := s; parse_rec rem
     | ("-inputenc" | "--inputenc") :: [] ->
-	usage ()
+        usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
-	Cdglobals.raw_comments := true; parse_rec rem
+        Cdglobals.raw_comments := true; parse_rec rem
     | ("-parse-comments" | "--parse-comments") :: rem ->
-	Cdglobals.parse_comments := true; parse_rec rem
+        Cdglobals.parse_comments := true; parse_rec rem
     | ("-plain-comments" | "--plain-comments") :: rem ->
-	Cdglobals.plain_comments := true; parse_rec rem
+        Cdglobals.plain_comments := true; parse_rec rem
     | ("-interpolate" | "--interpolate") :: rem ->
-	Cdglobals.interpolate := true; parse_rec rem
+        Cdglobals.interpolate := true; parse_rec rem
     | ("-toc-depth" | "--toc-depth") :: [] ->
       usage ()
     | ("-toc-depth" | "--toc-depth") :: ds :: rem ->
@@ -291,68 +291,68 @@ let parse () =
       parse_rec rem
 
     | ("-latin1" | "--latin1") :: rem ->
-	Cdglobals.set_latin1 (); parse_rec rem
+        Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
-	Cdglobals.set_utf8 (); parse_rec rem
+        Cdglobals.set_utf8 (); parse_rec rem
 
     | ("-q" | "-quiet" | "--quiet") :: rem ->
-	quiet := true; parse_rec rem
+        quiet := true; parse_rec rem
     | ("-v" | "-verbose" | "--verbose") :: rem ->
-	quiet := false; parse_rec rem
+        quiet := false; parse_rec rem
 
     | ("-h" | "-help" | "-?" | "--help") :: rem ->
-	banner (); usage ()
+        banner (); usage ()
     | ("-V" | "-version" | "--version") :: _ ->
-	banner (); exit 0
+        banner (); exit 0
 
     | ("-vernac-file" | "--vernac-file") :: f :: rem ->
-	check_if_file_exists f;
-	add_file (Vernac_file (f, coq_module f)); parse_rec rem
+        check_if_file_exists f;
+        add_file (Vernac_file (f, coq_module f)); parse_rec rem
     | ("-vernac-file" | "--vernac-file") :: [] ->
-	usage ()
+        usage ()
     | ("-tex-file" | "--tex-file") :: f :: rem ->
-	add_file (Latex_file f); parse_rec rem
+        add_file (Latex_file f); parse_rec rem
     | ("-tex-file" | "--tex-file") :: [] ->
-	usage ()
+        usage ()
     | ("-files" | "--files" | "--files-from") :: f :: rem ->
-	List.iter (fun f -> add_file (what_file f)) (files_from_file f);
-	parse_rec rem
+        List.iter (fun f -> add_file (what_file f)) (files_from_file f);
+        parse_rec rem
     | ("-files" | "--files") :: [] ->
-	usage ()
+        usage ()
     | "-R" :: path :: log :: rem ->
-	add_path path log; parse_rec rem
+        add_path path log; parse_rec rem
     | "-R" :: ([] | [_]) ->
-	usage ()
+        usage ()
     | "-Q" :: path :: log :: rem ->
-	add_path path log; parse_rec rem
+        add_path path log; parse_rec rem
     | "-Q" :: ([] | [_]) ->
-	usage ()
+        usage ()
     | ("-glob-from" | "--glob-from") :: f :: rem ->
-	glob_source := GlobFile f; parse_rec rem
+        glob_source := GlobFile f; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
-	usage ()
+        usage ()
     | ("-no-glob" | "--no-glob") :: rem ->
-	glob_source := NoGlob; parse_rec rem
+        glob_source := NoGlob; parse_rec rem
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
-	Cdglobals.externals := false; parse_rec rem
+        Cdglobals.externals := false; parse_rec rem
     | ("--external" | "-external") :: u :: logicalpath :: rem ->
-	Index.add_external_library logicalpath u; parse_rec rem
+        Index.add_external_library logicalpath u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: u :: rem ->
-	Cdglobals.coqlib := u; parse_rec rem
+        Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
-	usage ()
+        usage ()
     | ("--boot" | "-boot") :: rem ->
-	Cdglobals.coqlib_path := normalize_path (
+        Cdglobals.coqlib_path := normalize_path (
           Filename.concat
             (Filename.dirname Sys.executable_name)
             Filename.parent_dir_name
         ); parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
-	Cdglobals.coqlib_path := d; parse_rec rem
+        Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->
-	usage ()
+        usage ()
     | f :: rem ->
-	add_file (what_file f); parse_rec rem
+        add_file (what_file f); parse_rec rem
   in
     parse_rec (List.tl (Array.to_list Sys.argv));
     List.rev !files
@@ -424,13 +424,13 @@ let gen_mult_files l =
   let file = function
     | 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
+        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.trailer ();
-	  close_out_file()
+          open_out_file hf;
+          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;
@@ -486,14 +486,14 @@ let produce_document l =
   List.iter index_module l;
   match !out_to with
     | StdOut ->
-	Cdglobals.out_channel := stdout;
-	gen_one_file l
+        Cdglobals.out_channel := stdout;
+        gen_one_file l
     | File f ->
-	open_out_file f;
-	gen_one_file l;
-	close_out_file()
+        open_out_file f;
+        gen_one_file l;
+        close_out_file()
     | MultFiles ->
-	gen_mult_files l
+        gen_mult_files l
 
 let produce_output fl =
   if not (!dvi || !ps || !pdf) then
@@ -503,56 +503,56 @@ let produce_output fl =
       let texfile = Filename.temp_file "coqdoc" ".tex" in
       let basefile = Filename.chop_suffix texfile ".tex" in
       let final_out_to = !out_to in
-	out_to := File texfile;
-	output_dir := (Filename.dirname texfile);
-	produce_document fl;
-
-	let latexexe = if !pdf then "pdflatex" else "latex" in
-	let latexcmd =
-	  let file = Filename.basename texfile in
-	  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";
-	      clean_and_exit basefile res
-	    end;
-
-	  let dvifile = basefile ^ ".dvi" in
-	    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
+        out_to := File texfile;
+        output_dir := (Filename.dirname texfile);
+        produce_document fl;
+
+        let latexexe = if !pdf then "pdflatex" else "latex" in
+        let latexcmd =
+          let file = Filename.basename texfile in
+          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";
+              clean_and_exit basefile res
+            end;
+
+          let dvifile = basefile ^ ".dvi" in
+            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
             begin
-	        match final_out_to with
-		  | MultFiles | StdOut -> cat pdffile
-		  | File f -> copy pdffile f
-	    end;
-	    if !ps then begin
-	        let psfile = basefile ^ ".ps"
-		in
-		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";
-		      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
+                match final_out_to with
+                  | MultFiles | StdOut -> cat pdffile
+                  | File f -> copy pdffile f
+            end;
+            if !ps then begin
+                let psfile = basefile ^ ".ps"
+                in
+                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";
+                      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
 
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 02f0290802..5edf2b0d77 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -69,7 +69,7 @@ let is_keyword =
 let is_tactic =
   build_table
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
-      "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
+      "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor";
       "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
       "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto";
       "quote"; "eexact"; "autorewrite";
@@ -137,25 +137,25 @@ let initialize_tex_html () =
       (Tokens.ttree_add tt s l,
        match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l'))
       [ "*" ,  "\\ensuremath{\\times}", if_utf8 "×";
-	"|", "\\ensuremath{|}", None;
-	"->",  "\\ensuremath{\\rightarrow}", if_utf8 "→";
-	"->~",  "\\ensuremath{\\rightarrow\\lnot}", None;
-	"->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}", None;
-	"<-",  "\\ensuremath{\\leftarrow}", None;
-	"<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔";
-	"=>",  "\\ensuremath{\\Rightarrow}", if_utf8 "⇒";
-	"<=",  "\\ensuremath{\\le}", if_utf8 "≤";
-	">=",  "\\ensuremath{\\ge}", if_utf8 "≥";
-	"<>",  "\\ensuremath{\\not=}", if_utf8 "≠";
-	"~",   "\\ensuremath{\\lnot}", if_utf8 "¬";
-	"/\\", "\\ensuremath{\\land}", if_utf8 "∧";
-	"\\/", "\\ensuremath{\\lor}", if_utf8 "∨";
-	"|-",  "\\ensuremath{\\vdash}", None;
-	"forall", "\\ensuremath{\\forall}", if_utf8 "∀";
-	"exists", "\\ensuremath{\\exists}", if_utf8 "∃";
-	"Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
-	"λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
-	(* "fun", "\\ensuremath{\\lambda}" ? *)
+        "|", "\\ensuremath{|}", None;
+        "->",  "\\ensuremath{\\rightarrow}", if_utf8 "→";
+        "->~",  "\\ensuremath{\\rightarrow\\lnot}", None;
+        "->~~",  "\\ensuremath{\\rightarrow\\lnot\\lnot}", None;
+        "<-",  "\\ensuremath{\\leftarrow}", None;
+        "<->", "\\ensuremath{\\leftrightarrow}", if_utf8 "↔";
+        "=>",  "\\ensuremath{\\Rightarrow}", if_utf8 "⇒";
+        "<=",  "\\ensuremath{\\le}", if_utf8 "≤";
+        ">=",  "\\ensuremath{\\ge}", if_utf8 "≥";
+        "<>",  "\\ensuremath{\\not=}", if_utf8 "≠";
+        "~",   "\\ensuremath{\\lnot}", if_utf8 "¬";
+        "/\\", "\\ensuremath{\\land}", if_utf8 "∧";
+        "\\/", "\\ensuremath{\\lor}", if_utf8 "∨";
+        "|-",  "\\ensuremath{\\vdash}", None;
+        "forall", "\\ensuremath{\\forall}", if_utf8 "∀";
+        "exists", "\\ensuremath{\\exists}", if_utf8 "∃";
+        "Π", "\\ensuremath{\\Pi}", if_utf8 "Π";
+        "λ", "\\ensuremath{\\lambda}", if_utf8 "λ";
+        (* "fun", "\\ensuremath{\\lambda}" ? *)
       ] (Tokens.empty_ttree,Tokens.empty_ttree) in
   token_tree_latex := tree_latex;
   token_tree_html  := tree_html
@@ -243,13 +243,13 @@ module Latex = struct
 
   let char c = match c with
     | '\\' ->
-	printf "\\symbol{92}"
+        printf "\\symbol{92}"
     | '$' | '#' | '%' | '&' | '{' | '}' | '_' ->
-	output_char '\\'; output_char c
+        output_char '\\'; output_char c
     | '^' | '~' ->
-	output_char '\\'; output_char c; printf "{}"
+        output_char '\\'; output_char c; printf "{}"
     | _ ->
-	output_char c
+        output_char c
 
   let label_char c = match c with
     | '_' -> output_char ' '
@@ -273,22 +273,22 @@ module Latex = struct
     fun s ->
       Buffer.clear buff;
       for i = 0 to String.length s - 1 do
-	match s.[i] with
-	| '\\' ->
-	    Buffer.add_string buff "\\symbol{92}"
-	| '$' | '#' | '%' | '&' | '{' | '}' | '_' as c ->
-	    Buffer.add_char buff '\\'; Buffer.add_char buff c
-	| '^' | '~' as c ->
-	    Buffer.add_char buff '\\'; Buffer.add_char buff c;
-	    Buffer.add_string buff "{}"
+        match s.[i] with
+        | '\\' ->
+            Buffer.add_string buff "\\symbol{92}"
+        | '$' | '#' | '%' | '&' | '{' | '}' | '_' as c ->
+            Buffer.add_char buff '\\'; Buffer.add_char buff c
+        | '^' | '~' as c ->
+            Buffer.add_char buff '\\'; Buffer.add_char buff c;
+            Buffer.add_string buff "{}"
         | '\'' ->
             if i < String.length s - 1 && s.[i+1] = '\'' then begin
               Buffer.add_char buff '\''; Buffer.add_char buff '{';
               Buffer.add_char buff '}'
             end else
               Buffer.add_char buff '\''
-	| c ->
-	    Buffer.add_char buff c
+        | c ->
+            Buffer.add_char buff c
       done;
       Buffer.contents buff
 
@@ -310,8 +310,8 @@ module Latex = struct
 
   let start_quote () = output_char '`'; output_char '`'
   let stop_quote () = output_char '\''; output_char '\''
-    
-  let start_verbatim inline = 
+
+  let start_verbatim inline =
     if inline then printf "\\texttt{"
     else printf "\\begin{verbatim}"
 
@@ -319,7 +319,7 @@ module Latex = struct
     if inline then printf "}"
     else printf "\\end{verbatim}\n"
 
-  let url addr name = 
+  let url addr name =
     printf "%s\\footnote{\\url{%s}}"
       (match name with
        | None -> ""
@@ -337,16 +337,16 @@ module Latex = struct
     let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
       | Local ->
-	  if typ = Variable then
-	    printf "\\coqdoc%s{%s}" (type_name typ) s
-	  else
-	    (printf "\\coqref{"; label_ident id;
-	     printf "}{\\coqdoc%s{%s}}" (type_name typ) s)
+          if typ = Variable then
+            printf "\\coqdoc%s{%s}" (type_name typ) s
+          else
+            (printf "\\coqref{"; label_ident id;
+             printf "}{\\coqdoc%s{%s}}" (type_name typ) s)
       | External m when !externals ->
-	  printf "\\coqexternalref{"; label_ident fid;
-	  printf "}{%s}{\\coqdoc%s{%s}}" (escaped m) (type_name typ) s
+          printf "\\coqexternalref{"; label_ident fid;
+          printf "}{%s}{\\coqdoc%s{%s}}" (escaped m) (type_name typ) s
       | External _ | Unknown ->
-	  printf "\\coqdoc%s{%s}" (type_name typ) s
+          printf "\\coqdoc%s{%s}" (type_name typ) s
 
   let defref m id ty s =
     if ty <> Notation then
@@ -360,9 +360,9 @@ module Latex = struct
 
   let reference s = function
     | Def (fullid,typ) ->
-	defref (get_module false) fullid typ s
+        defref (get_module false) fullid typ s
     | Ref (m,fullid,typ) ->
-	ident_ref m fullid typ s
+        ident_ref m fullid typ s
 
   (*s The sublexer buffers symbol characters and attached
        uninterpreted ident and try to apply special translation such as,
@@ -407,7 +407,7 @@ module Latex = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
-  let keyword s loc = 
+  let keyword s loc =
     printf "\\coqdockw{%s}" (translate s)
 
   let ident s loc =
@@ -420,15 +420,15 @@ module Latex = struct
           reference (translate s) tag
     with Not_found ->
       if is_tactic s then
-	printf "\\coqdoctac{%s}" (translate s)
+        printf "\\coqdoctac{%s}" (translate s)
       else if is_keyword s then
-	printf "\\coqdockw{%s}" (translate s)
+        printf "\\coqdockw{%s}" (translate s)
       else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
       then
-	try
+        try
           let tag = Index.find_string s in
-	  reference (translate s) tag
-	with _ -> Tokens.output_tagged_ident_string s
+          reference (translate s) tag
+        with _ -> Tokens.output_tagged_ident_string s
       else Tokens.output_tagged_ident_string s
 
   let ident s l =
@@ -528,40 +528,40 @@ module Html = struct
     if !header_trailer then
       if !header_file_spec then
         let cin = open_in !header_file in
-	  try
-	    while true do
+          try
+            while true do
               let s = input_line cin in
-		printf "%s\n" s
-	    done
+                printf "%s\n" s
+            done
           with End_of_file -> close_in cin
       else
-	begin
-	  printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
-	  printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
-	  printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
-	  printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\" />\n" !charset;
-	  printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\" />\n";
-	  printf "<title>%s</title>\n</head>\n\n" !page_title;
-	  printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
-	  printf "<div id=\"main\">\n\n"
-	end
+        begin
+          printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
+          printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
+          printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
+          printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\" />\n" !charset;
+          printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\" />\n";
+          printf "<title>%s</title>\n</head>\n\n" !page_title;
+          printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
+          printf "<div id=\"main\">\n\n"
+        end
 
   let trailer () =
     if !header_trailer && !footer_file_spec then
         let cin = open_in !footer_file in
-	  try
-	    while true do
+          try
+            while true do
               let s = input_line cin in
-		printf "%s\n" s
-	    done
+                printf "%s\n" s
+            done
           with End_of_file -> close_in cin
     else
       begin
         if !index && (get_module false) <> "Index" then
           printf "</div>\n\n<div id=\"footer\">\n<hr/><a href=\"%s.html\">Index</a>" !index_name;
-	printf "<hr/>This page has been generated by ";
-	printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
-	printf "</div>\n\n</div>\n\n</body>\n</html>"
+        printf "<hr/>This page has been generated by ";
+        printf "<a href=\"%s\">coqdoc</a>\n" Coq_config.wwwcoq;
+        printf "</div>\n\n</div>\n\n</body>\n</html>"
       end
 
   let start_module () =
@@ -595,12 +595,12 @@ module Html = struct
     fun s ->
       Buffer.clear buff;
       for i = 0 to String.length s - 1 do
-	match s.[i] with
-	| '<' -> Buffer.add_string buff "&lt;"
-	| '>' -> Buffer.add_string buff "&gt;"
-	| '&' -> Buffer.add_string buff "&amp;"
+        match s.[i] with
+        | '<' -> Buffer.add_string buff "&lt;"
+        | '>' -> Buffer.add_string buff "&gt;"
+        | '&' -> Buffer.add_string buff "&amp;"
         | '\"' -> Buffer.add_string buff "&quot;"
-	| c -> Buffer.add_char buff c
+        | c -> Buffer.add_char buff c
       done;
       Buffer.contents buff
 
@@ -628,16 +628,16 @@ module Html = struct
   let start_quote () = char '"'
   let stop_quote () = start_quote ()
 
-  let start_verbatim inline = 
+  let start_verbatim inline =
     if inline then printf "<tt>"
     else printf "<pre>"
 
-  let stop_verbatim inline = 
-    if inline then printf "</tt>" 
+  let stop_verbatim inline =
+    if inline then printf "</tt>"
     else printf "</pre>\n"
 
-  let url addr name = 
-    printf "<a href=\"%s\">%s</a>" addr 
+  let url addr name =
+    printf "<a href=\"%s\">%s</a>" addr
       (match name with
        | Some n -> n
        | None -> addr)
@@ -645,29 +645,29 @@ module Html = struct
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
-	printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
+        printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
+        printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
     | External m when !externals ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
-	printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
+        printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
+        printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
     | External _ | Unknown ->
-	printf "<span class=\"id\" title=\"%s\">%s</span>" typ s
+        printf "<span class=\"id\" title=\"%s\">%s</span>" typ s
 
   let reference s r =
     match r with
     | Def (fullid,ty) ->
-	printf "<a name=\"%s\">" (sanitize_name fullid);
-	printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s
+        printf "<a name=\"%s\">" (sanitize_name fullid);
+        printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s
     | Ref (m,fullid,ty) ->
-	ident_ref m fullid (type_name ty) s
+        ident_ref m fullid (type_name ty) s
 
   let output_sublexer_string doescape issymbchar tag s =
     let s = if doescape then escaped s else s in
     match tag with
     | Some ref -> reference s ref
     | None ->
-	if issymbchar then output_string s
-	else printf "<span class=\"id\" title=\"var\">%s</span>" s
+        if issymbchar then output_string s
+        else printf "<span class=\"id\" title=\"var\">%s</span>" s
 
   let sublexer c loc =
     let tag =
@@ -686,7 +686,7 @@ module Html = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
-  let keyword s loc = 
+  let keyword s loc =
     printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
 
   let ident s loc =
@@ -697,14 +697,14 @@ module Html = struct
          reference (translate s) (Index.find (get_module false) loc)
     with Not_found ->
       if is_tactic s then
-	printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
+        printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
       else if is_keyword s then
         printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
       else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then
         try reference (translate s) (Index.find_string s)
-	with Not_found -> Tokens.output_tagged_ident_string s
+        with Not_found -> Tokens.output_tagged_ident_string s
       else
-	Tokens.output_tagged_ident_string s
+        Tokens.output_tagged_ident_string s
 
   let proofbox () = printf "<font size=-2>&#9744;</font>"
 
@@ -748,7 +748,7 @@ module Html = struct
 
   let end_code () = end_coq (); start_doc ()
 
-  let start_inline_coq () = 
+  let start_inline_coq () =
     if !inline_notmono then printf "<span class=\"inlinecodenm\">"
                        else printf "<span class=\"inlinecode\">"
 
@@ -758,7 +758,7 @@ module Html = struct
 
   let end_inline_coq_block () = end_inline_coq ()
 
-  let paragraph () = printf "\n<div class=\"paragraph\"> </div>\n\n" 
+  let paragraph () = printf "\n<div class=\"paragraph\"> </div>\n\n"
 
   (* inference rules *)
   let inf_rule assumptions (_,_,midnm) conclusions =
@@ -766,12 +766,12 @@ module Html = struct
        in a row with "&nbsp;"s.  We do this to the assumptions so that
        people can put multiple rules on a line with nice formatting *)
     let replace_spaces str =
-      let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in 
+      let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in
       let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in
       let strs = List.map (fun r -> match r with
                                     | Str.Text s  -> [s]
-                                    | Str.Delim s -> 
-                                        copy "&nbsp;" (String.length s))  
+                                    | Str.Delim s ->
+                                        copy "&nbsp;" (String.length s))
                           results
       in
         String.concat "" (List.concat strs)
@@ -782,7 +782,7 @@ module Html = struct
     let end_assumption () =
           (printf "  <td></td>\n";
            printf "</td>\n") in
-    let rec print_assumptions hyps = 
+    let rec print_assumptions hyps =
           match hyps with
           | []                 -> start_assumption "&nbsp;&nbsp;"
           | [(_,hyp)]          -> start_assumption hyp
@@ -793,7 +793,7 @@ module Html = struct
     print_assumptions assumptions;
     printf "  <td class=\"infrulenamecol\" rowspan=\"3\">\n";
     (match midnm with
-     | None   -> printf "    &nbsp;\n  </td>" 
+     | None   -> printf "    &nbsp;\n  </td>"
      | Some s -> printf "    %s &nbsp;\n  </td>" s);
     printf "</tr>\n";
     printf "<tr class=\"infrulemiddle\">\n";
@@ -827,9 +827,9 @@ module Html = struct
       let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in
       printf "<a name=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat;
       List.iter
-	(fun (id,(text,link,t)) ->
-	   let id' = prepare_entry id t in
-	   printf "<a href=\"%s\">%s</a> %s<br/>\n" link id' text) l;
+        (fun (id,(text,link,t)) ->
+           let id' = prepare_entry id t in
+           printf "<a href=\"%s\">%s</a> %s<br/>\n" link id' text) l;
       printf "<br/><br/>"
     end
 
@@ -840,35 +840,35 @@ module Html = struct
   let format_global_index =
     Index.map
       (fun s (m,t) ->
-	if t = Library then
+        if t = Library then
          let ln = !lib_name in
            if ln <> "" then
                "[" ^ String.lowercase_ascii ln ^ "]", m ^ ".html", t
            else
-	       "[library]", m ^ ".html", t
-	else
-	 sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
-	sprintf "%s.html#%s" m (sanitize_name s), t)
+               "[library]", m ^ ".html", t
+        else
+         sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
+        sprintf "%s.html#%s" m (sanitize_name s), t)
 
   let format_bytype_index = function
     | Library, idx ->
-	Index.map (fun id m -> "", m ^ ".html", Library) idx
+        Index.map (fun id m -> "", m ^ ".html", Library) idx
     | (t,idx) ->
-	Index.map
-	  (fun s m ->
-	     let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
-	       (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx
+        Index.map
+          (fun s m ->
+             let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
+               (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx
 
   (* Impression de la table d'index *)
   let print_index_table_item i =
     printf "<tr>\n<td>%s Index</td>\n" (String.capitalize_ascii i.idx_name);
     List.iter
       (fun (c,l) ->
-	 if l <> [] then
-	   printf "<td><a href=\"%s\">%s</a></td>\n" (index_ref i c)
-	     (display_letter c)
-	 else
-	   printf "<td>%s</td>\n" (display_letter c))
+         if l <> [] then
+           printf "<td><a href=\"%s\">%s</a></td>\n" (index_ref i c)
+             (display_letter c)
+         else
+           printf "<td>%s</td>\n" (display_letter c))
       i.idx_entries;
     let n = i.idx_size in
       printf "<td>(%d %s)</td>\n" n (if n > 1 then "entries" else "entry");
@@ -896,45 +896,45 @@ module Html = struct
   let make_multi_index () =
     let all_index =
       let glob,bt = Index.all_entries () in
-	(format_global_index glob) ::
-	  (List.map format_bytype_index bt) in
+        (format_global_index glob) ::
+          (List.map format_bytype_index bt) in
     let print_table () = print_index_table all_index in
       List.iter (make_one_multi_index print_table) all_index
 
   let make_index () =
     let all_index =
       let glob,bt = Index.all_entries () in
-	(format_global_index glob) ::
-	  (List.map format_bytype_index bt) in
+        (format_global_index glob) ::
+          (List.map format_bytype_index bt) in
     let print_table () = print_index_table all_index in
     let print_one_index i =
       if i.idx_size > 0 then begin
         printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize_ascii i.idx_name);
-	all_letters i
+        all_letters i
       end
     in
       set_module "Index" None;
       if !title <> "" then printf "<h1>%s</h1>\n" !title;
       print_table ();
       if not (!multi_index) then
-	begin
-	  List.iter print_one_index all_index;
-	  printf "<hr/>"; print_table ()
-	end
+        begin
+          List.iter print_one_index all_index;
+          printf "<hr/>"; print_table ()
+        end
 
     let make_toc () =
-	let ln = !lib_name in
+        let ln = !lib_name in
       let make_toc_entry = function
         | Toc_library (m,sub) ->
- 		stop_item ();
-		let ms = match sub with | None -> m | Some s -> m ^ ": " ^ s in
+                stop_item ();
+                let ms = match sub with | None -> m | Some s -> m ^ ": " ^ s in
               if ln = "" then
- 	          printf "<a href=\"%s.html\"><h2>%s</h2></a>\n" m ms
+                  printf "<a href=\"%s.html\"><h2>%s</h2></a>\n" m ms
               else
- 	          printf "<a href=\"%s.html\"><h2>%s %s</h2></a>\n" m ln ms
+                  printf "<a href=\"%s.html\"><h2>%s %s</h2></a>\n" m ln ms
         | Toc_section (n, f, r) ->
-  		item n;
-  		printf "<a href=\"%s\">" r; f (); printf "</a>\n"
+                item n;
+                printf "<a href=\"%s\">" r; f (); printf "</a>\n"
       in
         printf "<div id=\"toc\">\n";
         Queue.iter make_toc_entry toc_q;
@@ -990,7 +990,7 @@ module TeXmacs = struct
   let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
   let stop_verbatim inline = in_doc := false; printf "</verbatim>"
 
-  let url addr name = 
+  let url addr name =
     printf "%s<\\footnote><\\url>%s</url></footnote>" addr
       (match name with
        | None -> ""
@@ -1126,7 +1126,7 @@ module Raw = struct
   let start_verbatim inline = ()
   let stop_verbatim inline = ()
 
-  let url addr name = 
+  let url addr name =
     match name with
     | Some n -> printf "%s (%s)" n addr
     | None -> printf "%s" addr
@@ -1285,7 +1285,7 @@ let verbatim_char inline =
   select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
-let url = 
+let url =
   select Latex.url Html.url TeXmacs.url Raw.url
 
 let start_quote =
@@ -1293,15 +1293,15 @@ let start_quote =
 let stop_quote =
   select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
 
-let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = 
+let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions =
   start_verbatim false;
-  let dumb_line = 
+  let dumb_line =
        function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
                             char '\n')
-  in 
+  in
     (List.iter dumb_line assumptions;
-     dumb_line (midsp, midln ^ (match midnm with 
-                                | Some s -> " " ^ s 
+     dumb_line (midsp, midln ^ (match midnm with
+                                | Some s -> " " ^ s
                                 | None -> ""));
      List.iter dumb_line conclusions);
   stop_verbatim false
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index ceed67fff2..62da608348 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -98,7 +98,7 @@ val url : string -> string option -> unit
    something smart we can just format the rule verbatim like the user did
 *)
 val inf_rule :  (int * string) list
-             -> (int * string * (string option)) 
+             -> (int * string * (string option))
              -> (int * string) list
              -> unit
 
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 5adc18e1a0..0e7071425f 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -104,45 +104,45 @@ let buffer_char is_symbolchar ctag c =
       restart_buffering ()
   | Buffering (was_symbolchar,tag,translated,tt) ->
       if tag <> ctag then
-	(* A strong tag comes from Coq; if different Coq tags *)
-	(* hence, we don't try to see the chars as part of a single token *)
-	let translated =
-	  match tt.node with
-	  | Some tok -> Buffer.clear buff; tok
-	  | None -> translated in
-	flush_buffer was_symbolchar tag translated;
-	restart_buffering ()
+        (* A strong tag comes from Coq; if different Coq tags *)
+        (* hence, we don't try to see the chars as part of a single token *)
+        let translated =
+          match tt.node with
+          | Some tok -> Buffer.clear buff; tok
+          | None -> translated in
+        flush_buffer was_symbolchar tag translated;
+        restart_buffering ()
       else
-	begin
-	(* If we change the category of characters (symbol vs ident) *)
-	(* we accept this as a possible token cut point and remember the *)
-	(* translated token up to that point *)
-	let translated =
-	  if is_symbolchar <> was_symbolchar then
-	    match tt.node with
-	    | Some tok -> Buffer.clear buff; tok
-	    | None -> translated
-	  else translated in
-	(* We try to make a significant token from the current *)
-	(* buffer and the new character *)
-	try
-	  let tt = ttree_descend tt c in
-	  Buffer.add_char buff c;
-	  Buffering (is_symbolchar,ctag,translated,tt)
-	with Not_found ->
-	(* No existing translation for the given set of chars *)
-	if is_symbolchar <> was_symbolchar then
-	  (* If we changed the category of character read, we accept it *)
-	  (* as a possible cut point and restart looking for a translation *)
-	  (flush_buffer was_symbolchar tag translated;
-	   restart_buffering ())
-	else
-	  (* If we did not change the category of character read, we do *)
-	  (* not want to cut arbitrarily in the middle of the sequence of *)
-	  (*  symbol characters or identifier characters *)
-	  (Buffer.add_char buff c;
-	   Buffering (is_symbolchar,tag,translated,empty_ttree))
-	end
+        begin
+        (* If we change the category of characters (symbol vs ident) *)
+        (* we accept this as a possible token cut point and remember the *)
+        (* translated token up to that point *)
+        let translated =
+          if is_symbolchar <> was_symbolchar then
+            match tt.node with
+            | Some tok -> Buffer.clear buff; tok
+            | None -> translated
+          else translated in
+        (* We try to make a significant token from the current *)
+        (* buffer and the new character *)
+        try
+          let tt = ttree_descend tt c in
+          Buffer.add_char buff c;
+          Buffering (is_symbolchar,ctag,translated,tt)
+        with Not_found ->
+        (* No existing translation for the given set of chars *)
+        if is_symbolchar <> was_symbolchar then
+          (* If we changed the category of character read, we accept it *)
+          (* as a possible cut point and restart looking for a translation *)
+          (flush_buffer was_symbolchar tag translated;
+           restart_buffering ())
+        else
+          (* If we did not change the category of character read, we do *)
+          (* not want to cut arbitrarily in the middle of the sequence of *)
+          (*  symbol characters or identifier characters *)
+          (Buffer.add_char buff c;
+           Buffering (is_symbolchar,tag,translated,empty_ttree))
+        end
 
   and restart_buffering () =
     let tt = try ttree_descend !(!token_tree) c with Not_found -> empty_ttree in
@@ -163,9 +163,9 @@ let flush_sublexer () =
   | Neutral -> ()
   | Buffering (was_symbolchar,tag,translated,tt) ->
       let translated =
-	match tt.node with
-	| Some tok -> Buffer.clear buff; tok
-	| None -> translated in
+        match tt.node with
+        | Some tok -> Buffer.clear buff; tok
+        | None -> translated in
       flush_buffer was_symbolchar tag translated;
       translation_state := Neutral
 
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index 9f9c6dd5d0..343a61f44d 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -58,7 +58,7 @@ let read_fd fd s ~off ~len =
   let rec loop () =
     try Unix.read fd s off len
     with Unix.Unix_error(Unix.EAGAIN,_,_) -> loop ()
-  in 
+  in
     loop ()
 
 let really_read_fd fd s off len =
@@ -129,10 +129,10 @@ let chat s =
   try
     match parse_request (raw_input_line party.sock) with
     | Get n ->
-        if !cur_tokens < !max_tokens then allocate n party     
+        if !cur_tokens < !max_tokens then allocate n party
         else Queue.push (n,party) queue
     | TryGet n ->
-        if !cur_tokens < !max_tokens then allocate n party     
+        if !cur_tokens < !max_tokens then allocate n party
         else answer party Noluck
     | GiveBack n -> de_allocate n party
     | Ping ->
@@ -192,7 +192,7 @@ let main () =
     let pid = Unix.fork () in
     if pid <> 0 then begin
       Printf.printf "COQWORKMGR_SOCK=%s\n%!" str;
-      exit 0 
+      exit 0
     end else begin
       ignore(Unix.setsid ());
       Unix.close Unix.stdin;