[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
```

11 files changed, 84 insertions, 84 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
index 11d053624c..00ea8b8489 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -89,15 +89,15 @@ let gen_reference_in_modules locstr dirs s =
   match these with
     | [x] -> x
     | [] ->
-	anomaly ~label:locstr (str "cannot find " ++ str s ++
-	str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
+        anomaly ~label:locstr (str "cannot find " ++ str s ++
+        str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
         prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
     | l ->
       anomaly ~label:locstr
-	(str "ambiguous name " ++ str s ++ str " can represent " ++
-	   prlist_with_sep pr_comma
-	   (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
-	   str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
+        (str "ambiguous name " ++ str s ++ str " can represent " ++
+           prlist_with_sep pr_comma
+           (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
+           str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
            prlist_with_sep pr_comma DirPath.print dirs ++ str ".")
 
 (* For tactics/commands requiring vernacular libraries *)
diff --git a/library/coqlib.mli b/library/coqlib.mli
index ab8b18c4fb..10805416d1 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -210,9 +210,9 @@ val build_coq_f_equal2 : GlobRef.t delayed
 type coq_inversion_data = {
   inv_eq   : GlobRef.t; (** : forall params, args -> Prop *)
   inv_ind  : GlobRef.t; (** : forall params P (H : P params) args, eq params args
-			 ->  P args *)
+                         ->  P args *)
   inv_congr: GlobRef.t  (** : forall params B (f:t->B) args, eq params args ->
-			 f params = f args *)
+                         f params = f args *)
 }
 
 val build_coq_inversion_eq_data : coq_inversion_data delayed
diff --git a/library/global.ml b/library/global.ml
index 98d3e9cb1f..d4262683bb 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -201,10 +201,10 @@ let is_type_in_type r = is_type_in_type (env ()) r
 let current_modpath () =
   Safe_typing.current_modpath (safe_env ())
 
-let current_dirpath () = 
+let current_dirpath () =
   Safe_typing.current_dirpath (safe_env ())
 
-let with_global f = 
+let with_global f =
   let (a, ctx) = f (env ()) (current_dirpath ()) in
     push_context_set false ctx; a
 
diff --git a/library/global.mli b/library/global.mli
index 0570ad0102..db0f87df7e 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -105,7 +105,7 @@ val lookup_named     : variable -> Constr.named_declaration
 val lookup_constant  : Constant.t -> Opaqueproof.opaque Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
-val lookup_pinductive : Constr.pinductive -> 
+val lookup_pinductive : Constr.pinductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
 val lookup_mind      : MutInd.t -> Declarations.mutual_inductive_body
 val lookup_module    : ModPath.t -> Declarations.module_body
diff --git a/library/globnames.mli b/library/globnames.mli
index fc0de96e36..48cbb11b66 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -37,7 +37,7 @@ val subst_constructor : substitution -> constructor -> constructor
 val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
 val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
 
-(** This constr is not safe to be typechecked, universe polymorphism is not 
+(** This constr is not safe to be typechecked, universe polymorphism is not
     handled here: just use for printing *)
 val printable_constr_of_global : GlobRef.t -> constr
 
@@ -60,6 +60,6 @@ module ExtRefOrdered : sig
   val hash : t -> int
 end
 
-type global_reference_or_constr = 
+type global_reference_or_constr =
   | IsGlobal of GlobRef.t
   | IsConstr of constr
diff --git a/library/goptions.ml b/library/goptions.ml
index 0973944fb5..6e53bed349 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -52,12 +52,12 @@ type 'a table_of_A =  {
 module MakeTable =
   functor
    (A : sig
-	  type t
+          type t
           type key
           module Set : CSig.SetS with type elt = t
           val table : (string * key table_of_A) list ref
           val encode : Environ.env -> key -> t
-	  val subst : substitution -> t -> t
+          val subst : substitution -> t -> t
           val printer : t -> Pp.t
           val key : option_name
           val title : string
@@ -83,30 +83,30 @@ module MakeTable =
           | GOadd -> t := MySet.add p !t
           | GOrmv -> t := MySet.remove p !t in
         let load_options i o = if Int.equal i 1 then cache_options o in
-	let subst_options (subst,(f,p as obj)) = 
-	  let p' = A.subst subst p in
-	    if p' == p then obj else
-	      (f,p')
-	in
+        let subst_options (subst,(f,p as obj)) =
+          let p' = A.subst subst p in
+            if p' == p then obj else
+              (f,p')
+        in
         let inGo : option_mark * A.t -> obj =
           Libobject.declare_object {(Libobject.default_object nick) with
                 Libobject.load_function = load_options;
-		Libobject.open_function = load_options;
-		Libobject.cache_function = cache_options;
-		Libobject.subst_function = subst_options;
-		Libobject.classify_function = (fun x -> Substitute x)}
-	in
+                Libobject.open_function = load_options;
+                Libobject.cache_function = cache_options;
+                Libobject.subst_function = subst_options;
+                Libobject.classify_function = (fun x -> Substitute x)}
+        in
         ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
          (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
 
     let print_table table_name printer table =
       Feedback.msg_notice
         (str table_name ++
-	   (hov 0
-	      (if MySet.is_empty table then str " None" ++ fnl ()
+           (hov 0
+              (if MySet.is_empty table then str " None" ++ fnl ()
                else MySet.fold
-		 (fun a b -> spc () ++ printer a ++ b)
-		 table (mt ()) ++ str "." ++ fnl ())))
+                 (fun a b -> spc () ++ printer a ++ b)
+                 table (mt ()) ++ str "." ++ fnl ())))
 
     let table_of_A = {
        add = (fun env x -> add_option (A.encode env x));
diff --git a/library/lib.ml b/library/lib.ml
index 630c860a61..c3c480aee4 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -52,7 +52,7 @@ let subst_atomic_objects subst seg =
   let subst_one = fun (id,obj as node) ->
     let obj' = subst_object (subst,obj) in
       if obj' == obj then node else
-	(id, obj')
+        (id, obj')
   in
     List.Smart.map subst_one seg
 
@@ -296,15 +296,15 @@ let start_modtype = start_mod true None
 
 let error_still_opened string oname =
   let id = basename (fst oname) in
-  user_err 
+  user_err
     (str "The " ++ str string ++ str " " ++ Id.print id ++ str " is still opened.")
 
 let end_mod is_type =
   let oname,fs =
     try match find_entry_p is_opening_node with
       | oname,OpenedModule (ty,_,_,fs) ->
-	if ty == is_type then oname, fs
-	else error_still_opened (module_kind ty) oname
+        if ty == is_type then oname, fs
+        else error_still_opened (module_kind ty) oname
       | oname,OpenedSection _ -> error_still_opened "section" oname
       | _ -> assert false
     with Not_found -> user_err (Pp.str "No opened modules.")
@@ -359,7 +359,7 @@ let end_compilation_checks dir =
     match !lib_state.comp_name with
       | None -> anomaly (Pp.str "There should be a module name...")
       | Some m ->
-	  if not (Names.DirPath.equal m dir) then anomaly
+          if not (Names.DirPath.equal m dir) then anomaly
            (str "The current open module has name" ++ spc () ++ DirPath.print m ++
              spc () ++ str "and not" ++ spc () ++ DirPath.print m ++ str ".");
   in
diff --git a/library/libnames.ml b/library/libnames.ml
index 485f8837e8..126841c9a5 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -62,7 +62,7 @@ let parse_dir s =
     if n >= len then dirs else
     let pos =
       try
-	String.index_from s n '.'
+        String.index_from s n '.'
       with Not_found -> len
     in
     if Int.equal pos n then user_err Pp.(str @@ s ^ " is an invalid path.");
diff --git a/library/libobject.ml b/library/libobject.ml
index 932f065f73..a632a426fd 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -113,12 +113,12 @@ let declare_object_full odecl =
   and rebuild lobj = infun (odecl.rebuild_function (outfun lobj))
   in
   Hashtbl.add cache_tab na { dyn_cache_function = cacher;
-			     dyn_load_function = loader;
+                             dyn_load_function = loader;
                              dyn_open_function = opener;
-			     dyn_subst_function = substituter;
-			     dyn_classify_function = classifier;
-			     dyn_discharge_function = discharge;
-			     dyn_rebuild_function = rebuild };
+                             dyn_subst_function = substituter;
+                             dyn_classify_function = classifier;
+                             dyn_discharge_function = discharge;
+                             dyn_rebuild_function = rebuild };
   (infun,outfun)
 
 let declare_object odecl = fst (declare_object_full odecl)
@@ -144,7 +144,7 @@ let load_object i ((_,lobj) as node) =
 let open_object i ((_,lobj) as node) =
   apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj
 
-let subst_object ((_,lobj) as node) = 
+let subst_object ((_,lobj) as node) =
   apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj
 
 let classify_object lobj =
diff --git a/library/nametab.ml b/library/nametab.ml
index 8626ee1c59..283da5936c 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -128,7 +128,7 @@ struct
   (* Dictionaries of short names *)
   type nametree =
       { path : path_status;
-	map : nametree ModIdmap.t }
+        map : nametree ModIdmap.t }
 
   let mktree p m = { path=p; map=m }
   let empty_tree = mktree Nothing ModIdmap.empty
@@ -149,34 +149,34 @@ struct
             let ptab = modify () empty_tree in
             ModIdmap.add modid ptab tree.map
         in
-	let this =
+        let this =
           if level <= 0 then
-	    match tree.path with
-	      | Absolute (n,_) ->
-		  (* This is an absolute name, we must keep it
-		     otherwise it may become unaccessible forever *)
+            match tree.path with
+              | Absolute (n,_) ->
+                  (* This is an absolute name, we must keep it
+                     otherwise it may become unaccessible forever *)
                 warn_masking_absolute n; tree.path
-	      | Nothing
-	      | Relative _ -> Relative (uname,o)
+              | Nothing
+              | Relative _ -> Relative (uname,o)
           else tree.path
-	in
-	mktree this map
+        in
+        mktree this map
     | [] ->
-	match tree.path with
-	  | Absolute (uname',o') ->
-	      if E.equal o' o then begin
-		assert (U.equal uname uname');
-		tree
-		  (* we are putting the same thing for the second time :) *)
-	      end
-	      else
-		(* This is an absolute name, we must keep it otherwise it may
-		   become unaccessible forever *)
-		(* But ours is also absolute! This is an error! *)
-		user_err Pp.(str @@ "Cannot mask the absolute name \""
+        match tree.path with
+          | Absolute (uname',o') ->
+              if E.equal o' o then begin
+                assert (U.equal uname uname');
+                tree
+                  (* we are putting the same thing for the second time :) *)
+              end
+              else
+                (* This is an absolute name, we must keep it otherwise it may
+                   become unaccessible forever *)
+                (* But ours is also absolute! This is an error! *)
+                user_err Pp.(str @@ "Cannot mask the absolute name \""
                                    ^ U.to_string uname' ^ "\"!")
-	  | Nothing
-	  | Relative _ -> mktree (Absolute (uname,o)) tree.map
+          | Nothing
+          | Relative _ -> mktree (Absolute (uname,o)) tree.map
 
 let rec push_exactly uname o level tree = function
 | [] ->
@@ -241,7 +241,7 @@ let user_name qid tab =
 let find uname tab =
   let id,l = U.repr uname in
     match search (Id.Map.find id tab) l with
-	Absolute (_,o) -> o
+        Absolute (_,o) -> o
       | _ -> raise Not_found
 
 let exists uname tab =
@@ -260,9 +260,9 @@ let shortest_qualid ?loc ctx uname tab =
     | Absolute (u,_) | Relative (u,_)
           when U.equal u uname && not (is_empty && hidden) -> List.rev pos
     | _ ->
-	match dir with
-	    [] -> raise Not_found
-	  | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map)
+        match dir with
+            [] -> raise Not_found
+          | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map)
   in
   let ptab = Id.Map.find id tab in
   let found_dir = find_uname [] dir ptab in
@@ -385,25 +385,25 @@ let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevta
 let push_xref visibility sp xref =
   match visibility with
     | Until _ ->
-	the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
-	the_globrevtab := Globrevtab.add xref sp !the_globrevtab
+        the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
+        the_globrevtab := Globrevtab.add xref sp !the_globrevtab
     | _ ->
-	begin
-	  if ExtRefTab.exists sp !the_ccitab then
+        begin
+          if ExtRefTab.exists sp !the_ccitab then
             let open GlobRef in
-	    match ExtRefTab.find sp !the_ccitab with
-	      | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
-		    TrueGlobal( ConstructRef _) as xref ->
-		  the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
-	      | _ -> 
-		  the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
-	    else
-	      the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
-	end
+            match ExtRefTab.find sp !the_ccitab with
+              | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
+                    TrueGlobal( ConstructRef _) as xref ->
+                  the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
+              | _ ->
+                  the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
+            else
+              the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
+        end
 
 let push_cci visibility sp ref =
   push_xref visibility sp (TrueGlobal ref)
-    
+
 (* This is for Syntactic Definitions *)
 let push_syndef visibility sp kn =
   push_xref visibility sp (SynDef kn)
diff --git a/library/nametab.mli b/library/nametab.mli
index 55458fe2c6..d603bd51e2 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -100,7 +100,7 @@ val error_global_not_found : qualid -> 'a
    object is loaded inside a module -- or
    - for a precise suffix, when the module containing (the module
    containing ...) the object is opened (imported)
-   
+
 *)
 
 type visibility = Until of int | Exactly of int