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

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 544fd3d17d..1541e96635 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -64,8 +64,8 @@ type typeclass = {
 
   (* The method implementations as projections. *)
   cl_projs : (Name.t * (direction * hint_info) option
-	      * Constant.t option) list;
-  
+              * Constant.t option) list;
+
   cl_strict : bool;
 
   cl_unique : bool;
@@ -124,7 +124,7 @@ let class_of_constr env sigma c =
   try Some (dest_class_arity env sigma c)
   with e when CErrors.noncritical e -> None
 
-let is_class_constr sigma c = 
+let is_class_constr sigma c =
   try let gr, u = Termops.global_of_constr sigma c in
     GlobRef.Map.mem gr !classes
   with Not_found -> false
@@ -135,7 +135,7 @@ let rec is_class_type evd c =
     | Prod (_, _, t) -> is_class_type evd t
     | Cast (t, _, _) -> is_class_type evd t
     | _ -> is_class_constr evd c
-      
+
 let is_class_evar evd evi =
   is_class_type evd evi.Evd.evar_concl
 
@@ -160,7 +160,7 @@ let load_class cl =
 (** Build the subinstances hints. *)
 
 let check_instance env sigma c =
-  try 
+  try
     let (evd, c) = resolve_one_typeclass env sigma
       (Retyping.get_type_of env sigma c) in
       not (Evd.has_undefined evd)
@@ -168,8 +168,8 @@ let check_instance env sigma c =
 
 let build_subclasses ~check env sigma glob { hint_priority = pri } =
   let _id = Nametab.basename_of_global glob in
-  let _next_id = 
-    let i = ref (-1) in 
+  let _next_id =
+    let i = ref (-1) in
       (fun () -> incr i;
         Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
@@ -182,37 +182,37 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
       match class_of_constr env sigma ty with
       | None -> []
       | Some (rels, ((tc,u), args)) ->
-	let instapp = 
-	  Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
-	in
-	let instapp = EConstr.Unsafe.to_constr instapp in
-	let projargs = Array.of_list (args @ [instapp]) in
-	let projs = List.map_filter 
-	  (fun (n, b, proj) ->
-	   match b with 
-	   | None -> None
-	   | Some (Backward, _) -> None
-	   | Some (Forward, info) ->
-	     let proj = Option.get proj in
-	     let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in
-	     let u = EConstr.EInstance.kind sigma u in
-	     let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
-	       if check && check_instance env sigma (EConstr.of_constr body) then None
-	       else 
-		 let newpri =
-		   match pri, info.hint_priority with
-		   | Some p, Some p' -> Some (p + p')
-		   | Some p, None -> Some (p + 1)
-		   | _, _ -> None
-		 in
+        let instapp =
+          Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
+        in
+        let instapp = EConstr.Unsafe.to_constr instapp in
+        let projargs = Array.of_list (args @ [instapp]) in
+        let projs = List.map_filter
+          (fun (n, b, proj) ->
+           match b with
+           | None -> None
+           | Some (Backward, _) -> None
+           | Some (Forward, info) ->
+             let proj = Option.get proj in
+             let rels = List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) rels in
+             let u = EConstr.EInstance.kind sigma u in
+             let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
+               if check && check_instance env sigma (EConstr.of_constr body) then None
+               else
+                 let newpri =
+                   match pri, info.hint_priority with
+                   | Some p, Some p' -> Some (p + p')
+                   | Some p, None -> Some (p + 1)
+                   | _, _ -> None
+                 in
                    Some (GlobRef.ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
-	in
-	let declare_proj hints (cref, info, body) =
-	  let path' = cref :: path in
-	  let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in
-	  let rest = aux pri body ty path' in
-	    hints @ (path', info, body) :: rest
-	in List.fold_left declare_proj [] projs 
+        in
+        let declare_proj hints (cref, info, body) =
+          let path' = cref :: path in
+          let ty = Retyping.get_type_of env sigma (EConstr.of_constr body) in
+          let rest = aux pri body ty path' in
+            hints @ (path', info, body) :: rest
+        in List.fold_left declare_proj [] projs
   in
   let term = Constr.mkRef (glob, inst) in
     (*FIXME subclasses should now get substituted for each particular instance of
@@ -249,10 +249,10 @@ let instance_constructor (cl,u) args =
            applist (mkIndU ind, pars))
       | GlobRef.ConstRef cst ->
         let cst = cst, u in
-	let term = match args with
-	  | [] -> None
-	  | _ -> Some (List.last args)
-	in
+        let term = match args with
+          | [] -> None
+          | _ -> Some (List.last args)
+        in
           (term, applist (mkConstU cst, pars))
       | _ -> assert false
 
@@ -263,7 +263,7 @@ let cmap_elements c = GlobRef.Map.fold (fun k v acc -> v :: acc) c []
 let instances_of c =
   try cmap_elements (GlobRef.Map.find c.cl_impl !instances) with Not_found -> []
 
-let all_instances () = 
+let all_instances () =
   GlobRef.Map.fold (fun k v acc ->
     GlobRef.Map.fold (fun k v acc -> v :: acc) v acc)
     !instances []
@@ -271,7 +271,7 @@ let all_instances () =
 let instances env sigma r =
   let cl = class_info env sigma r in instances_of cl
 
-let is_class gr = 
+let is_class gr =
   GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
 
 open Evar_kinds