From 39f5e55e18afc15a9ed89508bcce4e3073c8b190 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 30 Oct 2019 23:36:37 +0100
Subject: [classes] Untabify in preparation for next commit.

---
 vernac/classes.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/vernac/classes.ml b/vernac/classes.ml
index cf668dfddb..42bc4e0d5c 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -47,7 +47,7 @@ let add_instance_hint inst path local info poly =
      in
      Flags.silently (fun () ->
        Hints.add_hints ~local [typeclasses_db]
-	  (Hints.HintsResolveEntry
+          (Hints.HintsResolveEntry
              [info, poly, false, Hints.PathHints path, inst'])) ()
 
 let is_local_for_hint i =
@@ -287,7 +287,7 @@ let type_ctx_instance ~program_mode env sigma ctx inst subst =
     decl :: ctx ->
       let t' = substl subst (RelDecl.get_type decl) in
       let (sigma, c'), l =
-	match decl with
+        match decl with
         | LocalAssum _ -> interp_casted_constr_evars ~program_mode env sigma (List.hd l) t', List.tl l
         | LocalDef (_,b,_) -> (sigma, substl subst b), l
       in
@@ -301,8 +301,8 @@ let id_of_class cl =
   match cl.cl_impl with
     | ConstRef kn -> Label.to_id @@ Constant.label kn
     | IndRef (kn,i) ->
-	let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
-	  mip.(0).Declarations.mind_typename
+        let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in
+          mip.(0).Declarations.mind_typename
     | _ -> assert false
 
 let instance_hook info global imps ?hook cst =
@@ -495,9 +495,9 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
       check_duplicate ?loc fs;
       let subst, sigma =
         do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in
-     let term, termtype =
-       do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
-     Some term, termtype, sigma
+      let term, termtype =
+        do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in
+      Some term, termtype, sigma
     | Some (_, term) ->
       let sigma, def =
         interp_casted_constr_evars ~program_mode:true env' sigma term cty in
-- 
cgit v1.2.3