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

1 files changed, 42 insertions, 42 deletions

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)