[lemmas] Untabify.

1 files changed, 17 insertions, 17 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e4415de8f2..f1d5412850 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -143,15 +143,15 @@ let adjust_guardness_conditions const = function
           match Constr.kind body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
 (*      let possible_indexes =
-	List.map2 (fun i c -> match i with Some i -> i | None ->
-	  List.interval 0 (List.length ((lam_assum c))))
-	  lemma_guard (Array.to_list fixdefs) in
+        List.map2 (fun i c -> match i with Some i -> i | None ->
+          List.interval 0 (List.length ((lam_assum c))))
+          lemma_guard (Array.to_list fixdefs) in
 *)
               let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
               let indexes =
                 search_guard env
                   possible_indexes fixdecls in
-		(mkFix ((indexes,0),fixdecls), ctx), eff
+                (mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
 
 let find_mutually_recursive_statements sigma thms =
@@ -189,23 +189,23 @@ let find_mutually_recursive_statements sigma thms =
     (* (degenerated cartesian product since there is at most one coind ccl) *)
     let same_indccl =
       List.cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] ind_ccls in
+        if List.for_all (of_same_mutind hyp) oks
+        then Some (hyp::oks) else None) [] ind_ccls in
     let ordered_same_indccl =
       List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in
     (* Check if some hypotheses are inductive in the same type *)
     let common_same_indhyp =
       List.cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] inds_hyps in
+        if List.for_all (of_same_mutind hyp) oks
+        then Some (hyp::oks) else None) [] inds_hyps in
     let ordered_inds,finite,guard =
       match ordered_same_indccl, common_same_indhyp with
       | indccl::rest, _ ->
-	  assert (List.is_empty rest);
+          assert (List.is_empty rest);
           (* One occ. of common coind ccls and no common inductive hyps *)
-	  if not (List.is_empty common_same_indhyp) then
-	    Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
-	  flush_all ();
+          if not (List.is_empty common_same_indhyp) then
+            Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
+          flush_all ();
           indccl, true, []
       | [], _::_ ->
           let () = match same_indccl with
@@ -220,10 +220,10 @@ let find_mutually_recursive_statements sigma thms =
           | _ -> ()
           in
           let possible_guards = List.map (List.map pi3) inds_hyps in
-	  (* assume the largest indices as possible *)
-	  List.last common_same_indhyp, false, possible_guards
+          (* assume the largest indices as possible *)
+          List.last common_same_indhyp, false, possible_guards
       | _, [] ->
-	  user_err Pp.(str
+        user_err Pp.(str
             ("Cannot find common (mutual) inductive premises or coinductive" ^
              " conclusions in the statements."))
     in
@@ -288,13 +288,13 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i
       match locality with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
-	  let c = SectionLocalDef const in
+          let c = SectionLocalDef const in
           let _ = declare_variable name (Lib.cwd(), c, k) in
           (VarRef name,impargs)
       | Global local ->
         let const =
           Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
-	in
+        in
         let kn = declare_constant name ~local (DefinitionEntry const, k) in
         (ConstRef kn,impargs)