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

12 files changed, 166 insertions, 166 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0dcc55a1cb..58c0f7db53 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -51,11 +51,11 @@ let refresh_undefined_univs clenv =
   match EConstr.kind clenv.evd clenv.templval.rebus with
   | Var _ -> clenv, Univ.empty_level_subst
   | App (f, args) when isVar clenv.evd f -> clenv, Univ.empty_level_subst
-  | _ ->  
+  | _ ->
     let evd', subst = Evd.refresh_undefined_universes clenv.evd in
     let map_freelisted f = { f with rebus = subst_univs_level_constr subst f.rebus } in
       { clenv with evd = evd'; templval = map_freelisted clenv.templval;
-	templtyp = map_freelisted clenv.templtyp }, subst
+        templtyp = map_freelisted clenv.templtyp }, subst
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
@@ -68,16 +68,16 @@ let clenv_push_prod cl =
   let rec clrec typ = match EConstr.kind cl.evd typ with
     | Cast (t,_,_) -> clrec t
     | Prod (na,t,u) ->
-	let mv = new_meta () in
-	let dep = not (noccurn (cl_sigma cl) 1 u) in
+        let mv = new_meta () in
+        let dep = not (noccurn (cl_sigma cl) 1 u) in
         let na' = if dep then na.binder_name else Anonymous in
         let e' = meta_declare mv t ~name:na' cl.evd in
-	let concl = if dep then subst1 (mkMeta mv) u else u in
-	let def = applist (cl.templval.rebus,[mkMeta mv]) in
-	{ templval = mk_freelisted def;
-	  templtyp = mk_freelisted concl;
-	  evd = e';
-	  env = cl.env }
+        let concl = if dep then subst1 (mkMeta mv) u else u in
+        let def = applist (cl.templval.rebus,[mkMeta mv]) in
+        { templval = mk_freelisted def;
+          templtyp = mk_freelisted concl;
+          evd = e';
+          env = cl.env }
     | _ -> raise NotExtensibleClause
   in clrec typ
 
@@ -102,12 +102,12 @@ let clenv_environments evd bound t =
       | (Some 0, _) -> (e, List.rev metas, t)
       | (n, Cast (t,_,_)) -> clrec (e,metas) n t
       | (n, Prod (na,t1,t2)) ->
-	  let mv = new_meta () in
-	  let dep = not (noccurn evd 1 t2) in
+          let mv = new_meta () in
+          let dep = not (noccurn evd 1 t2) in
           let na' = if dep then na.binder_name else Anonymous in
           let e' = meta_declare mv t1 ~name:na' e in
-	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
-	    (if dep then (subst1 (mkMeta mv) t2) else t2)
+          clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
+            (if dep then (subst1 (mkMeta mv) t2) else t2)
       | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
       | (n, _) -> (e, List.rev metas, t)
   in
@@ -167,7 +167,7 @@ let clenv_assign mv rhs clenv =
       if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
         error_incompatible_inst clenv mv
       else
-	clenv
+        clenv
     else
       let st = (Conv,TypeNotProcessed) in
       {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
@@ -226,8 +226,8 @@ let dependent_closure clenv mvs =
   let rec aux mvs acc =
     Metaset.fold
       (fun mv deps ->
-	let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in
-	aux metas_of_meta_type (Metaset.union deps metas_of_meta_type))
+        let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in
+        aux metas_of_meta_type (Metaset.union deps metas_of_meta_type))
       mvs acc in
   aux mvs mvs
 
@@ -241,9 +241,9 @@ let clenv_dependent_gen hyps_only ?(iter=true) clenv =
   List.filter
     (fun mv ->
       if hyps_only then
-	Metaset.mem mv deps_in_hyps && not (Metaset.mem mv deps_in_concl)
+        Metaset.mem mv deps_in_hyps && not (Metaset.mem mv deps_in_concl)
       else
-	Metaset.mem mv deps_in_hyps || Metaset.mem mv deps_in_concl)
+        Metaset.mem mv deps_in_hyps || Metaset.mem mv deps_in_concl)
     all_undefined
 
 let clenv_missing ce = clenv_dependent_gen true ce
@@ -336,8 +336,8 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
         let evd = clenv.evd in
-	let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
-	let clenv = clenv_assign mv evar {clenv with evd=evd} in
+        let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
+        let clenv = clenv_assign mv evar {clenv with evd=evd} in
         fold clenv (fst (destEvar evd evar) :: evs) mvs in
   fold clenv [] dep_mvs
 
@@ -415,13 +415,13 @@ let qhyp_eq h1 h2 = match h1, h2 with
 let check_bindings bl =
   match List.duplicates qhyp_eq (List.map (fun {CAst.v=x} -> fst x) bl) with
     | NamedHyp s :: _ ->
-	user_err 
-	  (str "The variable " ++ Id.print s ++
-	   str " occurs more than once in binding list.");
+        user_err
+          (str "The variable " ++ Id.print s ++
+           str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
-	user_err 
-	  (str "The position " ++ int n ++
-	   str " occurs more than once in binding list.")
+        user_err
+          (str "The position " ++ int n ++
+           str " occurs more than once in binding list.")
     | [] -> ()
 
 let explain_no_such_bound_variable evd id =
@@ -472,7 +472,7 @@ let meta_of_binder clause loc mvs = function
 let error_already_defined b =
   match b with
     | NamedHyp id ->
-        user_err 
+        user_err
           (str "Binder name \"" ++ Id.print id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
@@ -488,12 +488,12 @@ let clenv_unify_binding_type clenv c t u =
     try
       let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
       TypeProcessed, { clenv with evd = evd }, c
-    with 
+    with
       | PretypeError (_,_,ActualTypeNotCoercible (_,_,
           (NotClean _ | ConversionFailed _))) as e ->
-	  raise e
+          raise e
       | e when precatchable_exception e ->
-	  TypeNotProcessed, clenv, c
+          TypeNotProcessed, clenv, c
 
 let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
@@ -509,12 +509,12 @@ let clenv_match_args bl clenv =
     check_bindings bl;
     List.fold_left
       (fun clenv {CAst.loc;v=(b,c)} ->
-	let k = meta_of_binder clenv loc mvs b in
+        let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
           if EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
-	  clenv_assign_binding clenv k c)
+          clenv_assign_binding clenv k c)
       clenv bl
 
 exception NoSuchBinding
@@ -525,7 +525,7 @@ let clenv_constrain_last_binding c clenv =
   clenv_assign_binding clenv k c
 
 let error_not_right_number_missing_arguments n =
-  user_err 
+  user_err
     (strbrk "Not the right number of missing arguments (expected " ++
       int n ++ str ").")
 
@@ -538,14 +538,14 @@ let clenv_constrain_dep_args hyps_only bl clenv =
       List.fold_left2 clenv_assign_binding clenv occlist bl
     else
       if hyps_only then
-	(* Tolerance for compatibility <= 8.3 *)
-	let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in
-	if Int.equal (List.length occlist') (List.length bl) then
-	  List.fold_left2 clenv_assign_binding clenv occlist' bl
-	else
-	  error_not_right_number_missing_arguments (List.length occlist)
+        (* Tolerance for compatibility <= 8.3 *)
+        let occlist' = clenv_dependent_gen hyps_only ~iter:false clenv in
+        if Int.equal (List.length occlist') (List.length bl) then
+          List.fold_left2 clenv_assign_binding clenv occlist' bl
+        else
+          error_not_right_number_missing_arguments (List.length occlist)
       else
-	error_not_right_number_missing_arguments (List.length occlist)
+        error_not_right_number_missing_arguments (List.length occlist)
 
 (****************************************************************)
 (* Clausal environment for an application *)
@@ -557,7 +557,7 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
   | ExplicitBindings lbind ->
       let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in
       let clause = mk_clenv_from_env env sigma n
-	(c, t)
+        (c, t)
       in clenv_match_args lbind clause
   | NoBindings ->
       mk_clenv_from_env env sigma n (c,t)
@@ -567,7 +567,7 @@ let make_clenv_binding_env_apply env sigma n =
 
 let make_clenv_binding_env env sigma =
   make_clenv_binding_gen false None env sigma
-	
+
 let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma
 let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
 
@@ -659,7 +659,7 @@ let evar_with_name holes id =
   | [] -> explain_no_such_bound_variable holes id
   | [h] -> h.hole_evar
   | _ ->
-    user_err 
+    user_err
       (str "Binder name \"" ++ Id.print id ++
         str "\" occurs more than once in clause.")
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index eecd318287..3fca967395 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -24,10 +24,10 @@ open Tactypes
 
 type clausenv = {
   env      : env; (** the typing context *)
-  evd      : evar_map; (** the mapping from metavar and evar numbers to their 
-			   types and values *)
-  templval : constr freelisted; (** the template which we are trying to fill 
-				    out *)
+  evd      : evar_map; (** the mapping from metavar and evar numbers to their
+                           types and values *)
+  templval : constr freelisted; (** the template which we are trying to fill
+                                    out *)
   templtyp : constr freelisted (** its type *)}
 
 
@@ -92,8 +92,8 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
 
 (** start with a clenv to refine with a given term with bindings *)
 
-(** the arity of the lemma is fixed 
-   the optional int tells how many prods of the lemma have to be used 
+(** the arity of the lemma is fixed
+   the optional int tells how many prods of the lemma have to be used
    use all of them if None *)
 val make_clenv_binding_env_apply :
   env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings ->
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 8e7d1df29a..611671255d 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -35,15 +35,15 @@ let clenv_cast_meta clenv =
   and crec_hd u =
     match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with
       | Meta mv ->
-	  (try
+          (try
             let b = Typing.meta_type clenv.evd mv in
-	    assert (not (occur_meta clenv.evd b));
-	    if occur_meta clenv.evd b then u
+            assert (not (occur_meta clenv.evd b));
+            if occur_meta clenv.evd b then u
             else mkCast (mkMeta mv, DEFAULTcast, b)
-	  with Not_found -> u)
+          with Not_found -> u)
       | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
       | Case(ci,p,c,br) ->
-	  mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+          mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
       | Proj (p, c) -> mkProj (p, crec_hd c)
       | _ -> u
   in
@@ -130,6 +130,6 @@ let unify ?(flags=fail_quick_unif_flags) m =
     let evd = clear_metas (Tacmach.New.project gl) in
     try
       let evd' = w_unify env evd CONV ~flags m n in
-	Proofview.Unsafe.tclEVARSADVANCE evd'
+        Proofview.Unsafe.tclEVARSADVANCE evd'
     with e when CErrors.noncritical e -> Proofview.tclZERO e
   end
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 6c9c95e342..59918ab2f9 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -61,7 +61,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
-      user_err ?loc 
+      user_err ?loc
                 (str "Instance is not well-typed in the environment of " ++
                  Termops.pr_existential_key sigma evk ++ str ".")
   in
diff --git a/proofs/goal.ml b/proofs/goal.ml
index f95a904a5f..426fba7f63 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -121,12 +121,12 @@ module V82 = struct
       try ignore (Environ.lookup_named (NamedDecl.get_id decl) genv); false
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
-					  if is_proof_var decl then
+                                          if is_proof_var decl then
                                             let decl = Termops.map_named_decl EConstr.of_constr decl in
-					    mkNamedProd_or_LetIn decl t
-					  else
-					    t
-				       ) ~init:(concl sigma gl) env
+                                            mkNamedProd_or_LetIn decl t
+                                          else
+                                            t
+                                       ) ~init:(concl sigma gl) env
 
 end
 
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 46b54f9c2c..7b16d869e9 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -21,7 +21,7 @@ val uid : goal -> string
 (* Debugging help *)
 val pr_goal : goal -> Pp.t
 
-(* Layer to implement v8.2 tactic engine ontop of the new architecture. 
+(* Layer to implement v8.2 tactic engine ontop of the new architecture.
    Types are different from what they used to be due to a change of the
    internal types. *)
 module V82 : sig
@@ -42,7 +42,7 @@ module V82 : sig
   (* Old style mk_goal primitive, returns a new goal with corresponding
        hypotheses and conclusion, together with a term which is precisely
        the evar corresponding to the goal, and an updated evar_map. *)
-  val mk_goal : Evd.evar_map -> 
+  val mk_goal : Evd.evar_map ->
                          Environ.named_context_val ->
                          EConstr.constr ->
                          goal * EConstr.constr * Evd.evar_map
@@ -61,7 +61,7 @@ module V82 : sig
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
   (* Goal represented as a type, doesn't take into account section variables *)
-  val abstract_type : Evd.evar_map -> goal -> EConstr.types 
+  val abstract_type : Evd.evar_map -> goal -> EConstr.types
 
 end
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a9843e080e..a361c4208e 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -68,7 +68,7 @@ let catchable_exception = function
   (* reduction errors *)
   | Tacred.ReductionTacticError _ -> true
   (* unification and typing errors *)
-  | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e 
+  | PretypeError(_,_, e) -> is_unification_error e || is_typing_error e
   | _ -> false
 
 let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoSuchHyp id))
@@ -207,15 +207,15 @@ let split_sign env sigma hfrom hto l =
     | [] -> error_no_such_hypothesis env sigma hfrom
     | d :: right ->
         let hyp = NamedDecl.get_id d in
-      	if Id.equal hyp hfrom then
-	  (left,right,d, toleft || move_location_eq hto MoveLast)
-      	else
+        if Id.equal hyp hfrom then
+          (left,right,d, toleft || move_location_eq hto MoveLast)
+        else
           let is_toleft = match hto with
           | MoveAfter h' | MoveBefore h' -> Id.equal hyp h'
           | _ -> false
           in
-	  splitrec (d::left) (toleft || is_toleft)
-	    right
+          splitrec (d::left) (toleft || is_toleft)
+            right
   in
     splitrec [] false l
 
@@ -232,29 +232,29 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
   in
   let rec moverec first middle = function
     | [] ->
-	if match hto with MoveFirst | MoveLast -> false | _ -> true then
+        if match hto with MoveFirst | MoveLast -> false | _ -> true then
           error_no_such_hypothesis env sigma (hyp_of_move_location hto);
-	List.rev first @ List.rev middle
+        List.rev first @ List.rev middle
     | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
-	List.rev first @ List.rev middle @ right
+        List.rev first @ List.rev middle @ right
     | d :: right ->
         let hyp = NamedDecl.get_id d in
-	let (first',middle') =
-      	  if List.exists (test_dep d) middle then
-	    if not (move_location_eq hto (MoveAfter hyp)) then
-	      (first, d::middle)
+        let (first',middle') =
+          if List.exists (test_dep d) middle then
+            if not (move_location_eq hto (MoveAfter hyp)) then
+              (first, d::middle)
             else
-	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
+              user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
                 pr_move_location Id.print hto ++
-	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
-	        ++ Id.print hyp ++ str ".")
+                str (if toleft then ": it occurs in the type of " else ": it depends on ")
+                ++ Id.print hyp ++ str ".")
           else
-	    (d::first, middle)
-	in
-      	if move_location_eq hto (MoveAfter hyp) then
-	  List.rev first' @ List.rev middle' @ right
-      	else
-	  moverec first' middle' right
+            (d::first, middle)
+        in
+        if move_location_eq hto (MoveAfter hyp) then
+          List.rev first' @ List.rev middle' @ right
+        else
+          moverec first' middle' right
   in
   let open EConstr in
   if toleft then
@@ -265,7 +265,7 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
   else
     let right =
       List.fold_right push_named_context_val
-	(moverec [] [declfrom] right) empty_named_context_val in
+        (moverec [] [declfrom] right) empty_named_context_val in
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
@@ -328,7 +328,7 @@ exception Stop of EConstr.t list
 let meta_free_prefix sigma a =
   try
     let a = Array.map EConstr.of_constr a in
-    let _ = Array.fold_left (fun acc a -> 
+    let _ = Array.fold_left (fun acc a ->
       if occur_meta sigma a then raise (Stop acc)
       else a :: acc) [] a
     in a
@@ -355,69 +355,69 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
       match kind trm with
       | Meta _ ->
         let conclty = nf_betaiota env sigma (EConstr.of_constr conclty) in
-	  if !check && occur_meta sigma conclty then
+          if !check && occur_meta sigma conclty then
             raise (RefinerError (env, sigma, MetaInType conclty));
-	  let (gl,ev,sigma) = mk_goal hyps conclty in
-	  let ev = EConstr.Unsafe.to_constr ev in
-	  let conclty = EConstr.Unsafe.to_constr conclty in
-	  gl::goalacc, conclty, sigma, ev
+          let (gl,ev,sigma) = mk_goal hyps conclty in
+          let ev = EConstr.Unsafe.to_constr ev in
+          let conclty = EConstr.Unsafe.to_constr conclty in
+          gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
-	check_typability env sigma ty;
+        check_typability env sigma ty;
         let sigma = check_conv_leq_goal env sigma trm ty conclty in
-	let res = mk_refgoals sigma goal goalacc ty t in
+        let res = mk_refgoals sigma goal goalacc ty t in
         (* we keep the casts (in particular VMcast and NATIVEcast) except
            when they are annotating metas *)
-	if isMeta t then begin
-	  assert (k != VMcast && k != NATIVEcast);
-	  res
-	end else
-	  let (gls,cty,sigma,ans) = res in
+        if isMeta t then begin
+          assert (k != VMcast && k != NATIVEcast);
+          res
+        end else
+          let (gls,cty,sigma,ans) = res in
           let ans = if ans == t then trm else mkCast(ans,k,ty) in
-	  (gls,cty,sigma,ans)
+          (gls,cty,sigma,ans)
 
       | App (f,l) ->
-	let (acc',hdty,sigma,applicand) =
+        let (acc',hdty,sigma,applicand) =
           if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then
-	    let ty = 
-	      (* Template polymorphism of definitions and inductive types *)
-	      let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
-	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
-	        type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
-	    in
-	    let ty = EConstr.Unsafe.to_constr ty in
-	      goalacc, ty, sigma, f
-	  else
-	    mk_hdgoals sigma goal goalacc f
-	in
-	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
+            let ty =
+              (* Template polymorphism of definitions and inductive types *)
+              let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in
+              let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
+                type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
+            in
+            let ty = EConstr.Unsafe.to_constr ty in
+              goalacc, ty, sigma, f
+          else
+            mk_hdgoals sigma goal goalacc f
+        in
+        let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
         let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
         let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
         (acc'',conclty',sigma, ans)
 
       | Proj (p,c) ->
-	let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
-	let c = mkProj (p, c') in
-	let ty = get_type_of env sigma (EConstr.of_constr c) in
-	let ty = EConstr.Unsafe.to_constr ty in
-	  (acc',ty,sigma,c)
+        let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
+        let c = mkProj (p, c') in
+        let ty = get_type_of env sigma (EConstr.of_constr c) in
+        let ty = EConstr.Unsafe.to_constr ty in
+          (acc',ty,sigma,c)
 
       | Case (ci,p,c,lf) ->
-	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
-	let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
+        let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
+        let sigma = check_conv_leq_goal env sigma trm conclty' conclty in
         let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
         let lf' = Array.rev_of_list rbranches in
         let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
           else mkCase (ci,p',c',lf')
         in
-	(acc'',conclty',sigma, ans)
+        (acc'',conclty',sigma, ans)
 
       | _ ->
-	if occur_meta sigma (EConstr.of_constr trm) then
-	  anomaly (Pp.str "refiner called with a meta in non app/case subterm.");
-	let (sigma, t'ty) = goal_type_of env sigma trm in
-	let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
+        if occur_meta sigma (EConstr.of_constr trm) then
+          anomaly (Pp.str "refiner called with a meta in non app/case subterm.");
+        let (sigma, t'ty) = goal_type_of env sigma trm in
+        let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
           (goalacc,t'ty,sigma, trm)
 
 (* Same as mkREFGOALS but without knowing the type of the term. Therefore,
@@ -426,53 +426,53 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 and mk_hdgoals sigma goal goalacc trm =
   let env = Goal.V82.env sigma goal in
   let hyps = Goal.V82.hyps sigma goal in
-  let mk_goal hyps concl = 
+  let mk_goal hyps concl =
     Goal.V82.mk_goal sigma hyps concl in
   match kind trm with
     | Cast (c,_, ty) when isMeta c ->
-	check_typability env sigma ty;
+        check_typability env sigma ty;
         let (gl,ev,sigma) = mk_goal hyps (nf_betaiota env sigma (EConstr.of_constr ty)) in
-	let ev = EConstr.Unsafe.to_constr ev in
-	gl::goalacc,ty,sigma,ev
+        let ev = EConstr.Unsafe.to_constr ev in
+        gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
-	check_typability env sigma ty;
-	mk_refgoals sigma goal goalacc ty t
+        check_typability env sigma ty;
+        mk_refgoals sigma goal goalacc ty t
 
     | App (f,l) ->
-	let (acc',hdty,sigma,applicand) =
+        let (acc',hdty,sigma,applicand) =
           if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f)
-	  then
-	    let l' = meta_free_prefix sigma l in
-	   (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
-	  else mk_hdgoals sigma goal goalacc f
-	in
-	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
+          then
+            let l' = meta_free_prefix sigma l in
+           (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
+          else mk_hdgoals sigma goal goalacc f
+        in
+        let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
         let ans = if applicand == f && args == l then trm else mkApp (applicand, args) in
-	(acc'',conclty',sigma, ans)
+        (acc'',conclty',sigma, ans)
 
     | Case (ci,p,c,lf) ->
-	let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
+        let (acc',lbrty,conclty',sigma,p',c') = mk_casegoals sigma goal goalacc p c in
         let (acc'',sigma,rbranches) = treat_case sigma goal ci lbrty lf acc' in
-	let lf' = Array.rev_of_list rbranches in
-	let ans =
+        let lf' = Array.rev_of_list rbranches in
+        let ans =
           if p' == p && c' == c && Array.equal (==) lf' lf then trm
           else mkCase (ci,p',c',lf')
-	in
-	(acc'',conclty',sigma, ans)
+        in
+        (acc'',conclty',sigma, ans)
 
     | Proj (p,c) ->
          let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
-	 let c = mkProj (p, c') in
+         let c = mkProj (p, c') in
          let ty = get_type_of env sigma (EConstr.of_constr c) in
          let ty = EConstr.Unsafe.to_constr ty in
-	   (acc',ty,sigma,c)
+           (acc',ty,sigma,c)
 
     | _ ->
-	if !check && occur_meta sigma (EConstr.of_constr trm) then
-	  anomaly (Pp.str "refine called with a dependent meta.");
+        if !check && occur_meta sigma (EConstr.of_constr trm) then
+          anomaly (Pp.str "refine called with a dependent meta.");
         let (sigma, ty) = goal_type_of env sigma trm in
-	goalacc, ty, sigma, trm
+        goalacc, ty, sigma, trm
 
 and mk_arggoals sigma goal goalacc funty allargs =
   let foldmap (goalacc, funty, sigma) harg =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5f07cc1acc..2ee006631a 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -19,7 +19,7 @@
    - Focus: a proof has a focus stack: the top of the stack contains
      the context in which to unfocus the current view to a view focused
      with the rest of the stack.
-     In addition, this contains, for each of the focus context,  a 
+     In addition, this contains, for each of the focus context,  a
      "focus kind" and a "focus condition" (in practice, and for modularity,
      the focus kind is actually stored inside the condition). To unfocus, one
      needs to know the focus kind, and the condition (for instance "no condition" or
@@ -179,7 +179,7 @@ let cond_of_focus pr =
   | (cond,_,_)::_ -> cond
   | _ -> raise FullyUnfocused
 
-(* An auxiliary function to pop and read the last {!Proofview.focus_context} 
+(* An auxiliary function to pop and read the last {!Proofview.focus_context}
    on the focus stack. *)
 let pop_focus pr =
   match pr.focus_stack with
@@ -202,7 +202,7 @@ let _unfocus pr =
    { pr with proofview = Proofview.unfocus fc pr.proofview }
 
 (* Focus command (focuses on the [i]th subgoal) *)
-(* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
+(* spiwack: there could also, easily be a focus-on-a-range tactic, is there
    a need for it? *)
 let focus cond inf i pr =
   try _focus cond (Obj.repr inf) i i pr
@@ -250,7 +250,7 @@ let rec unfocus kind pr () =
   | Loose ->
     begin try
             let pr = _unfocus pr in
-	    unfocus kind pr ()
+            unfocus kind pr ()
       with FullyUnfocused -> raise CannotUnfocusThisWay
     end
 
@@ -412,7 +412,7 @@ module V82 = struct
 
   let top_goal p =
     let { Evd.it=gls ; sigma=sigma; } =
-	Proofview.V82.top_goals p.entry p.proofview
+        Proofview.V82.top_goals p.entry p.proofview
     in
     { Evd.it=List.hd gls ; sigma=sigma; }
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 9973df492d..134b0146b6 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -19,7 +19,7 @@
    - Focus: a proof has a focus stack: the top of the stack contains
      the context in which to unfocus the current view to a view focused
      with the rest of the stack.
-     In addition, this contains, for each of the focus context,  a 
+     In addition, this contains, for each of the focus context,  a
      "focus kind" and a "focus condition" (in practice, and for modularity,
      the focus kind is actually stored inside the condition). To unfocus, one
      needs to know the focus kind, and the condition (for instance "no condition" or
@@ -107,7 +107,7 @@ val new_focus_kind : unit -> 'a focus_kind
     the action which focused.
     Conditions always carry a focus kind, and inherit their type parameter
     from it.*)
-type 'a focus_condition 
+type 'a focus_condition
 (* [no_cond] only checks that the unfocusing command uses the right
     [focus_kind].
    If [loose_end] (default [false]) is [true], then if the [focus_kind]
@@ -126,7 +126,7 @@ val no_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
 val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
 
 (* focus command (focuses on the [i]th subgoal) *)
-(* spiwack: there could also, easily be a focus-on-a-range tactic, is there 
+(* spiwack: there could also, easily be a focus-on-a-range tactic, is there
    a need for it? *)
 val focus : 'a focus_condition -> 'a -> int -> t -> t
 
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 5702156b65..66e2ae5c29 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -50,7 +50,7 @@ module Strict = struct
   | Suggest of t (* this bullet is mandatory here *)
   | Unfinished of t (* no mandatory bullet here, but this bullet is unfinished *)
   | NoBulletInUse (* No mandatory bullet (or brace) here, no bullet pending,
-      	       some focused goals exists. *)
+               some focused goals exists. *)
   | NeedClosingBrace (* Some unfocussed goal exists "{" needed to focus them *)
   | ProofFinished (* No more goal anywhere *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index e1896d51e3..832a749ef2 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -89,7 +89,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) =
   let gll =
       (List.map_i (fun i ->
         apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
-	0 gs) in
+        0 gs) in
     (sigr,List.flatten gll)
 
 (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
@@ -188,13 +188,13 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
       (fun hypl -> List.subtract cmp hypl oldhyps)
       hyps
   in
-  let s = 
+  let s =
     let frst = ref true in
     List.fold_left
     (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
       ^ (List.fold_left
-	   (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc)
-	   "" lh))
+           (fun acc d -> (Names.Id.to_string (NamedDecl.get_id d)) ^ " " ^ acc)
+           "" lh))
     "" newhyps in
   Feedback.msg_notice
     (str "<infoH>"
@@ -273,5 +273,5 @@ let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
 
 (* Change evars *)
 let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma}
-let tclPUSHEVARUNIVCONTEXT ctx gl = 
+let tclPUSHEVARUNIVCONTEXT ctx gl =
   tclEVARS (Evd.merge_universe_context (project gl) ctx) gl
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index def67abad7..aed1c89bfe 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -43,7 +43,7 @@ val pf_get_hyp_typ        : Goal.goal sigma -> Id.t -> types
 val pf_get_new_id         : Id.t -> Goal.goal sigma -> Id.t
 
 val pf_apply : (env -> evar_map -> 'a) -> Goal.goal sigma -> 'a
-val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) -> 
+val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) ->
   Goal.goal sigma -> 'a -> Goal.goal sigma * 'b
 val pf_reduce :
   (env -> evar_map -> constr -> constr) ->