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

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0178d5c009..2db674d397 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -29,7 +29,7 @@ exception Find_at of int
 (* profiling *)
 
 let profiling_enabled = ref false
-    
+
 (* for supported platforms, filename for profiler results *)
 
 let profile_filename = ref "native_compute_profile.data"
@@ -52,8 +52,8 @@ let set_profile_filename fn =
 (* find unused profile filename *)
 let get_available_profile_filename () =
   let profile_filename = get_profile_filename () in
-  let dir = Filename.dirname profile_filename in 
-  let base = Filename.basename profile_filename in 
+  let dir = Filename.dirname profile_filename in
+  let base = Filename.basename profile_filename in
   (* starting with OCaml 4.04, could use Filename.remove_extension and Filename.extension, which
      gets rid of need for exception-handling here
   *)
@@ -65,7 +65,7 @@ let get_available_profile_filename () =
       (nm,ex)
     with Invalid_argument _ -> (base,"")
   in
-  try 
+  try
     (* unlikely race: fn deleted, another process uses fn *)
     Filename.temp_file ~temp_dir:dir (name ^ "_") ext
   with Sys_error s ->
@@ -75,16 +75,16 @@ let get_available_profile_filename () =
 
 let get_profiling_enabled () =
   !profiling_enabled
-    
+
 let set_profiling_enabled b =
   profiling_enabled := b
-    
+
 let invert_tag cst tag reloc_tbl =
   try
     for j = 0 to Array.length reloc_tbl - 1 do
       let tagj,arity = reloc_tbl.(j) in
       if Int.equal tag tagj && (cst && Int.equal arity 0 || not(cst || Int.equal arity 0)) then
-	raise (Find_at j)
+        raise (Find_at j)
       else ()
     done;raise Not_found
   with Find_at j -> (j+1)
@@ -101,7 +101,7 @@ let app_type env c =
   let t = whd_all env c in
   try destApp t with DestKO -> (t,[||])
 
- 
+
 let find_rectype_a env c =
   let (t, l) = app_type env c in
   match kind t with
@@ -117,7 +117,7 @@ let type_constructor mind mib u (ctx, typ) params =
   let nparams = Array.length params in
   if Int.equal nparams 0 then ctyp
   else
-    let _,ctyp = decompose_prod_n nparams ctyp in   
+    let _,ctyp = decompose_prod_n nparams ctyp in
     substl (List.rev (Array.to_list params)) ctyp
 
 let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
@@ -127,12 +127,12 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   let i = invert_tag const tag mip.mind_reloc_tbl in
   let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(i-1)) params in
   (mkApp(mkConstructU((ind,i),u), params), ctyp)
- 
+
 
 let construct_of_constr const env sigma tag typ =
   let t, l = app_type env typ in
   match EConstr.kind_upto sigma t with
-  | Ind (ind,u) -> 
+  | Ind (ind,u) ->
       construct_of_constr_notnative const env tag ind u l
   | _ ->
     assert (Constr.equal t (Typeops.type_of_int env));
@@ -165,7 +165,7 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params p =
       let params = Array.map (lift ndecl) params in
       let dep_cstr = mkApp(mkApp(mkConstructU (cstr,snd ind),params),relargs) in
       mkApp(papp,[|dep_cstr|])
-    in 
+    in
     decl, decl_with_letin, codom
   in Array.mapi build_one_branch mip.mind_nf_lc
 
@@ -174,11 +174,11 @@ let build_case_type p realargs c =
 
 (* normalisation of values *)
 
-let branch_of_switch lvl ans bs = 
+let branch_of_switch lvl ans bs =
   let tbl = ans.asw_reloc in
-  let branch i = 
+  let branch i =
     let tag,arity = tbl.(i) in
-    let ci = 
+    let ci =
       if Int.equal arity 0 then mk_const tag
       else mk_block tag (mk_rels_accu lvl arity) in
     bs ci in
@@ -195,11 +195,11 @@ let get_proj env (ind, proj_arg) =
 let rec nf_val env sigma v typ =
   match kind_of_value v with
   | Vaccu accu -> nf_accu env sigma accu
-  | Vfun f -> 
+  | Vfun f ->
       let lvl = nb_rel env in
       let name,dom,codom =
-	try decompose_prod env typ
-	with DestKO ->
+        try decompose_prod env typ
+        with DestKO ->
           CErrors.anomaly
             (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
       in
@@ -221,7 +221,7 @@ and nf_type env sigma v =
 
 and nf_type_sort env sigma v =
   match kind_of_value v with
-  | Vaccu accu -> 
+  | Vaccu accu ->
       let t,s = nf_accu_type env sigma accu in
       let s =
         try
@@ -249,12 +249,12 @@ and nf_accu_type env sigma accu =
     mkApp(a,Array.of_list args), t
 
 and nf_args env sigma args t =
-  let aux arg (t,l) = 
+  let aux arg (t,l) =
     let _,dom,codom =
       try decompose_prod env t with
-	DestKO ->
-	CErrors.anomaly
-	  (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+        DestKO ->
+        CErrors.anomaly
+          (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
     in
     let c = nf_val env sigma arg dom in
     (subst1 c codom, c::l)
@@ -268,10 +268,10 @@ and nf_bargs env sigma b t =
   Array.init len
     (fun i ->
       let _,dom,codom =
-	try decompose_prod env !t with
-	  DestKO ->
-	  CErrors.anomaly
-	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+        try decompose_prod env !t with
+          DestKO ->
+          CErrors.anomaly
+            (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
       in
       let c = nf_val env sigma (block_field b i) dom in
       t := subst1 c codom; c)
@@ -318,9 +318,9 @@ and nf_atom_type env sigma atom =
       let nparams = mib.mind_nparams in
       let params,realargs = Array.chop nparams allargs in
       let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
-      let pT = 
+      let pT =
         hnf_prod_applist_assum env nparamdecls
-	  (Inductiveops.type_of_inductive env ind) (Array.to_list params) in
+          (Inductiveops.type_of_inductive env ind) (Array.to_list params) in
       let p = nf_predicate env sigma ind mip params p pT in
       (* Calcul du type des branches *)
       let btypes = build_branches_type env sigma (fst ind) mib mip u params p in
@@ -330,11 +330,11 @@ and nf_atom_type env sigma atom =
        let decl,decl_with_letin,codom = btypes.(i) in
        let b = nf_val (Termops.push_rels_assum decl env) sigma v codom in
         Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin
-      in 
+      in
       let branchs = Array.mapi mkbranch bsw in
       let tcase = build_case_type p realargs a in
       let ci = ans.asw_ci in
-      mkCase(ci, p, a, branchs), tcase 
+      mkCase(ci, p, a, branchs), tcase
   | Afix(tt,ft,rp,s) ->
       let tt = Array.map (fun t -> nf_type_sort env sigma t) tt in
       let tt = Array.map fst tt and rt = Array.map snd tt in
@@ -393,7 +393,7 @@ and  nf_predicate env sigma ind mip params v pT =
       let k = nb_rel env in
       let vb = f (mk_rel_accu k) in
       let body =
-	nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
+        nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
       mkLambda(name,dom,body)
     | _ -> nf_type env sigma v
     end
@@ -444,23 +444,23 @@ let start_profiler_linux profile_fn =
   let dev_null = Unix.descr_of_out_channel (open_out_bin "/dev/null") in
   let _ = Feedback.msg_info (Pp.str ("Profiling to file " ^ profile_fn)) in
   let perf = "perf" in
-  let profiler_pid = 
+  let profiler_pid =
     Unix.create_process
       perf
       [|perf; "record"; "-g"; "-o"; profile_fn; "-p"; string_of_int coq_pid |]
       Unix.stdin dev_null dev_null
   in
   (* doesn't seem to be a way to test whether process creation succeeded *)
-  if !Flags.debug then 
+  if !Flags.debug then
     Feedback.msg_debug (Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn));
   Some profiler_pid
 
 (* kill profiler via SIGINT *)
-let stop_profiler_linux m_pid = 
-  match m_pid with 
+let stop_profiler_linux m_pid =
+  match m_pid with
   | Some pid -> (
     let _ = if !Flags.debug then Feedback.msg_debug (Pp.str "Stopping native code profiler") in
-    try 
+    try
       Unix.kill pid Sys.sigint;
       let _ = Unix.waitpid [] pid in ()
     with Unix.Unix_error (Unix.ESRCH,"kill","") ->
@@ -475,7 +475,7 @@ let start_profiler () =
   | _ ->
      let _ = Feedback.msg_info
        (Pp.str (Format.sprintf "Native_compute profiling not supported on the platform: %s"
-		  (profiler_platform ()))) in
+                  (profiler_platform ()))) in
      None
 
 let stop_profiler m_pid =