[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, 72 insertions, 72 deletions

diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index c341ec8d57..c41b0d7a02 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -50,13 +50,13 @@ let pp_abst st = function
   | [] -> assert false
   | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
   | l -> paren
-	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
+        (str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
 
 let pp_apply st _ = function
   | [] -> st
   | [a] -> hov 2 (paren (st ++ spc () ++ a))
   | args -> hov 2 (paren (str "@ " ++ st ++
-			  (prlist_strict (fun x -> spc () ++ x) args)))
+                          (prlist_strict (fun x -> spc () ++ x) args)))
 
 (*s The pretty-printer for Scheme syntax *)
 
@@ -68,66 +68,66 @@ let rec pp_expr env args =
   let apply st = pp_apply st true args in
   function
     | MLrel n ->
-	let id = get_db_name n env in apply (pr_id id)
+        let id = get_db_name n env in apply (pr_id id)
     | MLapp (f,args') ->
-	let stl = List.map (pp_expr env []) args' in
+        let stl = List.map (pp_expr env []) args' in
         pp_expr env (stl @ args) f
     | MLlam _ as a ->
-      	let fl,a' = collect_lams a in
-	let fl,env' = push_vars (List.map id_of_mlid fl) env in
-	apply (pp_abst (pp_expr env' [] a') (List.rev fl))
+        let fl,a' = collect_lams a in
+        let fl,env' = push_vars (List.map id_of_mlid fl) env in
+        apply (pp_abst (pp_expr env' [] a') (List.rev fl))
     | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id_of_mlid id] env in
-	apply
-	  (hv 0
-	     (hov 2
-		(paren
-		   (str "let " ++
-		    paren
-		      (paren
-			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1))
-		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
+        let i,env' = push_vars [id_of_mlid id] env in
+        apply
+          (hv 0
+             (hov 2
+                (paren
+                   (str "let " ++
+                    paren
+                      (paren
+                         (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1))
+                    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r ->
-	apply (pp_global Term r)
+        apply (pp_global Term r)
     | MLcons (_,r,args') ->
-	assert (List.is_empty args);
-	let st =
-	  str "`" ++
-	  paren (pp_global Cons r ++
-		 (if List.is_empty args' then mt () else spc ()) ++
-		 prlist_with_sep spc (pp_cons_args env) args')
-	in
-	if is_coinductive r then paren (str "delay " ++ st) else st
+        assert (List.is_empty args);
+        let st =
+          str "`" ++
+          paren (pp_global Cons r ++
+                 (if List.is_empty args' then mt () else spc ()) ++
+                 prlist_with_sep spc (pp_cons_args env) args')
+        in
+        if is_coinductive r then paren (str "delay " ++ st) else st
     | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Scheme yet.")
     | MLcase (_,_,pv) when not (is_regular_match pv) ->
-	user_err Pp.(str "Cannot handle general patterns in Scheme yet.")
+        user_err Pp.(str "Cannot handle general patterns in Scheme yet.")
     | MLcase (_,t,pv) when is_custom_match pv ->
-	let mkfun (ids,_,e) =
-	  if not (List.is_empty ids) then named_lams (List.rev ids) e
-	  else dummy_lams (ast_lift 1 e) 1
-	in
-	apply
-	  (paren
-	     (hov 2
-		(str (find_custom_match pv) ++ fnl () ++
-		 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
-		 ++ pp_expr env [] t)))
+        let mkfun (ids,_,e) =
+          if not (List.is_empty ids) then named_lams (List.rev ids) e
+          else dummy_lams (ast_lift 1 e) 1
+        in
+        apply
+          (paren
+             (hov 2
+                (str (find_custom_match pv) ++ fnl () ++
+                 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
+                 ++ pp_expr env [] t)))
     | MLcase (typ,t, pv) ->
         let e =
-	  if not (is_coinductive_type typ) then pp_expr env [] t
-	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
-	in
-	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
+          if not (is_coinductive_type typ) then pp_expr env [] t
+          else paren (str "force" ++ spc () ++ pp_expr env [] t)
+        in
+        apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
     | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix env' i (Array.of_list (List.rev ids'),defs) args
+        let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+        pp_fix env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s ->
-	(* An [MLexn] may be applied, but I don't really care. *)
-	paren (str "error" ++ spc () ++ qs s)
+        (* An [MLexn] may be applied, but I don't really care. *)
+        paren (str "error" ++ spc () ++ qs s)
     | MLdummy _ ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
+        str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLmagic a ->
-	pp_expr env args a
+        pp_expr env args a
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
     | MLuint _ ->
       paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
@@ -137,8 +137,8 @@ let rec pp_expr env args =
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->
       paren (pp_global Cons r ++
-	     (if List.is_empty args then mt () else spc ()) ++
-	     prlist_with_sep spc (pp_cons_args env) args)
+             (if List.is_empty args then mt () else spc ()) ++
+             prlist_with_sep spc (pp_cons_args env) args)
   | e -> str "," ++ pp_expr env [] e
 
 and pp_one_pat env (ids,p,t) =
@@ -166,12 +166,12 @@ and pp_fix env j (ids,bl) args =
     paren
       (str "letrec " ++
        (v 0 (paren
-	       (prvect_with_sep fnl
-		  (fun (fi,ti) ->
-		     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
-		  (Array.map2 (fun id b -> (id,b)) ids bl)) ++
-	     fnl () ++
-      	     hov 2 (pp_apply (pr_id (ids.(j))) true args))))
+               (prvect_with_sep fnl
+                  (fun (fi,ti) ->
+                     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
+                  (Array.map2 (fun id b -> (id,b)) ids bl)) ++
+             fnl () ++
+             hov 2 (pp_apply (pr_id (ids.(j))) true args))))
 
 (*s Pretty-printing of a declaration. *)
 
@@ -180,29 +180,29 @@ let pp_decl = function
   | Dtype _ -> mt ()
   | Dfix (rv, defs,_) ->
       let names = Array.map
-	(fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+        (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
       in
       prvecti
-	(fun i r ->
-	  let void = is_inline_custom r ||
-	    (not (is_custom r) &&
+        (fun i r ->
+          let void = is_inline_custom r ||
+            (not (is_custom r) &&
              match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
-	  in
-	  if void then mt ()
-	  else
-	    hov 2
-	      (paren (str "define " ++ names.(i) ++ spc () ++
-			(if is_custom r then str (find_custom r)
-			 else pp_expr (empty_env ()) [] defs.(i)))
-	       ++ fnl ()) ++ fnl ())
-	rv
+          in
+          if void then mt ()
+          else
+            hov 2
+              (paren (str "define " ++ names.(i) ++ spc () ++
+                        (if is_custom r then str (find_custom r)
+                         else pp_expr (empty_env ()) [] defs.(i)))
+               ++ fnl ()) ++ fnl ())
+        rv
   | Dterm (r, a, _) ->
       if is_inline_custom r then mt ()
       else
-	hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
-			(if is_custom r then str (find_custom r)
-			 else pp_expr (empty_env ()) [] a)))
-	++ fnl2 ()
+        hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
+                        (if is_custom r then str (find_custom r)
+                         else pp_expr (empty_env ()) [] a)))
+        ++ fnl2 ()
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d