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

9 files changed, 818 insertions, 818 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 1c325a8d3a..2f3f42c5f6 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -164,9 +164,9 @@ let rename_tvars avoid l =
   let rec rename avoid = function
     | [] -> [],avoid
     | id :: idl ->
-	let id = rename_id (lowercase_id id) avoid in
-	let idl, avoid = rename (Id.Set.add id avoid) idl in
-	(id :: idl, avoid) in
+        let id = rename_id (lowercase_id id) avoid in
+        let idl, avoid = rename (Id.Set.add id avoid) idl in
+        (id :: idl, avoid) in
   fst (rename avoid l)
 
 let push_vars ids (db,avoid) =
@@ -271,8 +271,8 @@ let params_ren_add, params_ren_mem =
 *)
 
 type visible_layer = { mp : ModPath.t;
-		       params : ModPath.t list;
-		       mutable content : Label.t KMap.t; }
+                       params : ModPath.t list;
+                       mutable content : Label.t KMap.t; }
 
 let pop_visible, push_visible, get_visible =
   let vis = ref [] in
@@ -281,10 +281,10 @@ let pop_visible, push_visible, get_visible =
     match !vis with
       | [] -> assert false
       | v :: vl ->
-	  vis := vl;
-	  (* we save the 1st-level-content of MPfile for later use *)
-	  if get_phase () == Impl && modular () && is_modfile v.mp
-	  then add_mpfiles_content v.mp v.content
+          vis := vl;
+          (* we save the 1st-level-content of MPfile for later use *)
+          if get_phase () == Impl && modular () && is_modfile v.mp
+          then add_mpfiles_content v.mp v.content
   and push mp mps =
     vis := { mp = mp; params = mps; content = KMap.empty } :: !vis
   and get () = !vis
@@ -356,9 +356,9 @@ let modfstlev_rename =
     with Not_found ->
       let s = ascii_of_id id in
       if is_lower s || begins_with_CoqXX s then
-	(add_index id 1; "Coq_"^s)
+        (add_index id 1; "Coq_"^s)
       else
-	(add_index id 0; s)
+        (add_index id 0; s)
 
 (*s Creating renaming for a [module_path] : first, the real function ... *)
 
@@ -448,13 +448,13 @@ let visible_clash mp0 ks =
     | [] -> false
     | v :: _ when ModPath.equal v.mp mp0 -> false
     | v :: vis ->
-	let b = KMap.mem ks v.content in
-	if b && not (is_mp_bound mp0) then true
-	else begin
-	  if b then params_ren_add mp0;
-	  if params_lookup mp0 ks v.params then false
-	  else clash vis
-	end
+        let b = KMap.mem ks v.content in
+        if b && not (is_mp_bound mp0) then true
+        else begin
+          if b then params_ren_add mp0;
+          if params_lookup mp0 ks v.params then false
+          else clash vis
+        end
   in clash (get_visible ())
 
 (* Same, but with verbose output (and mp0 shouldn't be a MPbound) *)
@@ -464,10 +464,10 @@ let visible_clash_dbg mp0 ks =
     | [] -> None
     | v :: _ when ModPath.equal v.mp mp0 -> None
     | v :: vis ->
-	try Some (v.mp,KMap.find ks v.content)
-	with Not_found ->
-	  if params_lookup mp0 ks v.params then None
-	  else clash vis
+        try Some (v.mp,KMap.find ks v.content)
+        with Not_found ->
+          if params_lookup mp0 ks v.params then None
+          else clash vis
   in clash (get_visible ())
 
 (* After the 1st pass, we can decide which modules will be opened initially *)
@@ -483,9 +483,9 @@ let opened_libraries () =
        after such an open, there's no unambiguous way to refer to objects of B. *)
     let to_open =
       List.filter
-	(fun mp ->
-	   not (List.exists (fun k -> KMap.mem k (get_mpfiles_content mp)) used_ks))
-	used_files
+        (fun mp ->
+           not (List.exists (fun k -> KMap.mem k (get_mpfiles_content mp)) used_ks))
+        used_files
     in
     mpfiles_clear ();
     List.iter mpfiles_add to_open;
@@ -549,18 +549,18 @@ let pp_ocaml_extern k base rls = match rls with
   | [] -> assert false
   | base_s :: rls' ->
       if (not (modular ())) (* Pseudo qualification with "" *)
-	|| (List.is_empty rls')  (* Case of a file A.v used as a module later *)
-	|| (not (mpfiles_mem base)) (* Module not opened *)
-	|| (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *)
-	|| (visible_clash base (fstlev_ks k rls')) (* Local conflict *)
+        || (List.is_empty rls')  (* Case of a file A.v used as a module later *)
+        || (not (mpfiles_mem base)) (* Module not opened *)
+        || (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *)
+        || (visible_clash base (fstlev_ks k rls')) (* Local conflict *)
       then
-	(* We need to fully qualify. Last clash situation is unsupported *)
-	match visible_clash_dbg base (Mod,base_s) with
-	  | None -> dottify rls
-	  | Some (mp,l) -> error_module_clash base (MPdot (mp,l))
+        (* We need to fully qualify. Last clash situation is unsupported *)
+        match visible_clash_dbg base (Mod,base_s) with
+          | None -> dottify rls
+          | Some (mp,l) -> error_module_clash base (MPdot (mp,l))
       else
-	(* Standard situation : object in an opened file *)
-	dottify rls'
+        (* Standard situation : object in an opened file *)
+        dottify rls'
 
 (* [pp_ocaml_gen] : choosing between [pp_ocaml_local] or [pp_ocaml_extern] *)
 
@@ -568,9 +568,9 @@ let pp_ocaml_gen k mp rls olab =
   match common_prefix_from_list mp (get_visible_mps ()) with
     | Some prefix -> pp_ocaml_local k prefix mp rls olab
     | None ->
-	let base = base_mp mp in
-	if is_mp_bound base then pp_ocaml_bound base rls
-	else pp_ocaml_extern k base rls
+        let base = base_mp mp in
+        if is_mp_bound base then pp_ocaml_bound base rls
+        else pp_ocaml_extern k base rls
 
 (* For Haskell, things are simpler: we have removed (almost) all structures *)
 
@@ -607,9 +607,9 @@ let pp_module mp =
   match mp with
     | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) ->
         (* simplest situation: definition of mp (or use in the same context) *)
-	(* we update the visible environment *)
-	let s = List.hd ls in
-	add_visible (Mod,s) l; s
+        (* we update the visible environment *)
+        let s = List.hd ls in
+        add_visible (Mod,s) l; s
     | _ -> pp_ocaml_gen Mod mp (List.rev ls) None
 
 (** Special hack for constants of type Ascii.ascii : if an
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 551dbdc6fb..35110552ab 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -147,8 +147,8 @@ let check_fix env sg cb i =
     | Def lbody ->
         (match EConstr.kind sg (get_body lbody) with
           | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
-	  | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
-	  | _ -> raise Impossible)
+          | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
+          | _ -> raise Impossible)
     | Undef _ | OpaqueDef _ | Primitive _ -> raise Impossible
 
 let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) =
@@ -166,14 +166,14 @@ let factor_fix env sg l cb msb =
     let labels = Array.make n l in
     List.iteri
       (fun j ->
-	 function
-	   | (l,SFBconst cb') ->
+         function
+           | (l,SFBconst cb') ->
               let check' = check_fix env sg cb' (j+1) in
               if not ((fst check : bool) == (fst check') &&
                         prec_declaration_equal sg (snd check) (snd check'))
-	       then raise Impossible;
-	       labels.(j+1) <- l;
-	   | _ -> raise Impossible) msb';
+               then raise Impossible;
+               labels.(j+1) <- l;
+           | _ -> raise Impossible) msb';
     labels, recd, msb''
   end
 
@@ -256,8 +256,8 @@ and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with
       let sg = Evd.from_env env in
       (match extract_with_type env' sg (EConstr.of_constr c) with
        (* cb may contain some kn *)
-	 | None -> mt
-	 | Some (vl,typ) ->
+         | None -> mt
+         | Some (vl,typ) ->
             type_iter_references Visit.add_ref typ;
             MTwith(mt,ML_With_type(idl,vl,typ)))
   | MEwith(me',WithMod(idl,mp))->
@@ -271,8 +271,8 @@ and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with
 and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MoreFunctor (mbid, mtb, me_alg') ->
       let me_struct' = match me_struct with
-	| MoreFunctor (mbid',_,me') when MBId.equal mbid' mbid -> me'
-	| _ -> assert false
+        | MoreFunctor (mbid',_,me') when MBId.equal mbid' mbid -> me'
+        | _ -> assert false
       in
       let mp = MPbound mbid in
       let env' = Modops.add_module_type mp mtb env in
@@ -288,7 +288,7 @@ and extract_msignature_spec env mp1 reso = function
       let mp = MPbound mbid in
       let env' = Modops.add_module_type mp mtb env in
       MTfunsig (mbid, extract_mbody_spec env mp mtb,
-		extract_msignature_spec env' mp1 reso me)
+                extract_msignature_spec env' mp1 reso me)
 
 and extract_mbody_spec : 'a. _ -> _ -> 'a generic_module_body -> _ =
   fun env mp mb -> match mb.mod_type_alg with
@@ -308,38 +308,38 @@ let rec extract_structure env mp reso ~all = function
       (try
          let sg = Evd.from_env env in
          let vl,recd,struc = factor_fix env sg l cb struc in
-	 let vc = Array.map (make_cst reso mp) vl in
-	 let ms = extract_structure env mp reso ~all struc in
-	 let b = Array.exists Visit.needed_cst vc in
-	 if all || b then
+         let vc = Array.map (make_cst reso mp) vl in
+         let ms = extract_structure env mp reso ~all struc in
+         let b = Array.exists Visit.needed_cst vc in
+         if all || b then
            let d = extract_fixpoint env sg vc recd in
-	   if (not b) && (logical_decl d) then ms
-	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
-	 else ms
+           if (not b) && (logical_decl d) then ms
+           else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
+         else ms
        with Impossible ->
-	 let ms = extract_structure env mp reso ~all struc in
-	 let c = make_cst reso mp l in
-	 let b = Visit.needed_cst c in
-	 if all || b then
-	   let d = extract_constant env c cb in
-	   if (not b) && (logical_decl d) then ms
-	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
-	 else ms)
+         let ms = extract_structure env mp reso ~all struc in
+         let c = make_cst reso mp l in
+         let b = Visit.needed_cst c in
+         if all || b then
+           let d = extract_constant env c cb in
+           if (not b) && (logical_decl d) then ms
+           else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
+         else ms)
   | (l,SFBmind mib) :: struc ->
       let ms = extract_structure env mp reso ~all struc in
       let mind = make_mind reso mp l in
       let b = Visit.needed_ind mind in
       if all || b then
-	let d = Dind (mind, extract_inductive env mind) in
-	if (not b) && (logical_decl d) then ms
-	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
+        let d = Dind (mind, extract_inductive env mind) in
+        if (not b) && (logical_decl d) then ms
+        else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
       else ms
   | (l,SFBmodule mb) :: struc ->
       let ms = extract_structure env mp reso ~all struc in
       let mp = MPdot (mp,l) in
       let all' = all || Visit.needed_mp_all mp in
       if all' || Visit.needed_mp mp then
-	(l,SEmodule (extract_module env mp ~all:all' mb)) :: ms
+        (l,SEmodule (extract_module env mp ~all:all' mb)) :: ms
       else ms
   | (l,SFBmodtype mtb) :: struc ->
       let ms = extract_structure env mp reso ~all struc in
@@ -363,7 +363,7 @@ and extract_mexpr env mp = function
       Visit.add_mp_all mp; Miniml.MEident mp
   | MEapply (me, arg) ->
       Miniml.MEapply (extract_mexpr env mp me,
-	              extract_mexpr env mp (MEident arg))
+                      extract_mexpr env mp (MEident arg))
 
 and extract_mexpression env mp = function
   | NoFunctor me -> extract_mexpr env mp me
@@ -373,7 +373,7 @@ and extract_mexpression env mp = function
       Miniml.MEfunctor
         (mbid,
          extract_mbody_spec env mp1 mtb,
-	 extract_mexpression env' mp me)
+         extract_mexpression env' mp me)
 
 and extract_msignature env mp reso ~all = function
   | NoFunctor struc ->
@@ -385,7 +385,7 @@ and extract_msignature env mp reso ~all = function
       Miniml.MEfunctor
         (mbid,
          extract_mbody_spec env mp1 mtb,
-	 extract_msignature env' mp reso ~all me)
+         extract_msignature env' mp reso ~all me)
 
 and extract_module env mp ~all mb =
   (* A module has an empty [mod_expr] when :
@@ -447,19 +447,19 @@ let mono_filename f =
   match f with
     | None -> None, None, default_id
     | Some f ->
-	let f =
-	  if Filename.check_suffix f d.file_suffix then
-	    Filename.chop_suffix f d.file_suffix
-	  else f
-	in
-	let id =
-	  if lang () != Haskell then default_id
-	  else
+        let f =
+          if Filename.check_suffix f d.file_suffix then
+            Filename.chop_suffix f d.file_suffix
+          else f
+        in
+        let id =
+          if lang () != Haskell then default_id
+          else
             try Id.of_string (Filename.basename f)
-	    with UserError _ ->
+            with UserError _ ->
               user_err Pp.(str "Extraction: provided filename is not a valid identifier")
-	in
-	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
+        in
+        Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
 
 (* Builds a suitable filename from a module id *)
 
@@ -494,8 +494,8 @@ let formatter dry file =
     if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
     else
       match file with
-	| Some f -> Topfmt.with_output_to f
-	| None -> Format.formatter_of_buffer buf
+        | Some f -> Topfmt.with_output_to f
+        | None -> Format.formatter_of_buffer buf
   in
   (* XXX: Fixme, this shouldn't depend on Topfmt *)
   (* We never want to see ellipsis ... in extracted code *)
@@ -554,14 +554,14 @@ let print_structure_to_file (fn,si,mo) dry struc =
        let cout = open_out si in
        let ft = formatter false (Some cout) in
        begin try
-	 set_phase Intf;
-	 pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
-	 pp_with ft (d.pp_sig (signature_of_structure struc));
+         set_phase Intf;
+         pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
+         pp_with ft (d.pp_sig (signature_of_structure struc));
          Format.pp_print_flush ft ();
-	 close_out cout;
+         close_out cout;
        with reraise ->
          Format.pp_print_flush ft ();
-	 close_out cout; raise reraise
+         close_out cout; raise reraise
        end;
        info_file si)
     (if dry then None else si);
@@ -606,9 +606,9 @@ let rec locate_ref = function
       in
       match mpo, ro with
         | None, None -> Nametab.error_global_not_found qid
-	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
-	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
-	| Some mp, Some r ->
+        | None, Some r -> let refs,mps = locate_ref l in r::refs,mps
+        | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
+        | Some mp, Some r ->
            warning_ambiguous_name (qid,mp,r);
            let refs,mps = locate_ref l in refs,mp::mps
 
@@ -637,7 +637,7 @@ let separate_extraction lr =
   warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
-	print_structure_to_file (module_filename mp) false [e]
+        print_structure_to_file (module_filename mp) false [e]
     | _ -> assert false
   in
   List.iter print struc;
@@ -686,8 +686,8 @@ let extraction_library is_rec m =
   warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
-	let dry = not is_rec && not (DirPath.equal dir dir_m) in
-	print_structure_to_file (module_filename mp) dry [e]
+        let dry = not is_rec && not (DirPath.equal dir dir_m) in
+        print_structure_to_file (module_filename mp) dry [e]
     | _ -> assert false
   in
   List.iter print struc;
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 04f5b66241..a4469b7ec1 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -243,8 +243,8 @@ let parse_ind_args si args relmax =
     | Kill _ :: s -> parse (i+1) j s
     | Keep :: s ->
       (match Constr.kind args.(i-1) with
-	 | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s)
-	 | _ -> parse (i+1) (j+1) s)
+         | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s)
+         | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
 
 (*S Extraction of a type. *)
@@ -265,31 +265,31 @@ let rec extract_type env sg db j c args =
         extract_type env sg db j d (Array.to_list args' @ args)
     | Lambda (_,_,d) ->
         (match args with
-	   | [] -> assert false (* A lambda cannot be a type. *)
+           | [] -> assert false (* A lambda cannot be a type. *)
            | a :: args -> extract_type env sg db j (EConstr.Vars.subst1 a d) args)
     | Prod (n,t,d) ->
         assert (List.is_empty args);
         let env' = push_rel_assum (n,t) env in
         (match flag_of_type env sg t with
            | (Info, Default) ->
-	       (* Standard case: two [extract_type] ... *)
+               (* Standard case: two [extract_type] ... *)
                let mld = extract_type env' sg (0::db) j d [] in
-	       (match expand env mld with
-		  | Tdummy d -> Tdummy d
+               (match expand env mld with
+                  | Tdummy d -> Tdummy d
                   | _ -> Tarr (extract_type env sg db 0 t [], mld))
-	   | (Info, TypeScheme) when j > 0 ->
-	       (* A new type var. *)
+           | (Info, TypeScheme) when j > 0 ->
+               (* A new type var. *)
                let mld = extract_type env' sg (j::db) (j+1) d [] in
-	       (match expand env mld with
-		  | Tdummy d -> Tdummy d
-		  | _ -> Tarr (Tdummy Ktype, mld))
-	   | _,lvl ->
+               (match expand env mld with
+                  | Tdummy d -> Tdummy d
+                  | _ -> Tarr (Tdummy Ktype, mld))
+           | _,lvl ->
                let mld = extract_type env' sg (0::db) j d [] in
-	       (match expand env mld with
-		  | Tdummy d -> Tdummy d
-		  | _ ->
-		      let reason = if lvl == TypeScheme then Ktype else Kprop in
-		      Tarr (Tdummy reason, mld)))
+               (match expand env mld with
+                  | Tdummy d -> Tdummy d
+                  | _ ->
+                      let reason = if lvl == TypeScheme then Ktype else Kprop in
+                      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
     | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop
     | Rel n ->
@@ -297,16 +297,16 @@ let rec extract_type env sg db j c args =
            | LocalDef (_,t,_) ->
                extract_type env sg db j (EConstr.Vars.lift n t) args
            | _ ->
-	       (* Asks [db] a translation for [n]. *)
-	       if n > List.length db then Tunknown
-	       else let n' = List.nth db (n-1) in
-	       if Int.equal n' 0 then Tunknown else Tvar n')
+               (* Asks [db] a translation for [n]. *)
+               if n > List.length db then Tunknown
+               else let n' = List.nth db (n-1) in
+               if Int.equal n' 0 then Tunknown else Tvar n')
     | Const (kn,u) ->
         let r = GlobRef.ConstRef kn in
         let typ = type_of env sg (EConstr.mkConstU (kn,u)) in
         (match flag_of_type env sg typ with
-	   | (Logic,_) -> assert false (* Cf. logical cases above *)
-	   | (Info, TypeScheme) ->
+           | (Logic,_) -> assert false (* Cf. logical cases above *)
+           | (Info, TypeScheme) ->
                let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in
                (match (lookup_constant kn env).const_body with
                  | Undef _ | OpaqueDef _ | Primitive _ -> mlt
@@ -314,18 +314,18 @@ let rec extract_type env sg db j c args =
                  | Def lbody ->
                       let newc = applistc (get_body lbody) args in
                       let mlt' = extract_type env sg db j newc [] in
-		      (* ML type abbreviations interact badly with Coq *)
-		      (* reduction, so [mlt] and [mlt'] might be different: *)
-		      (* The more precise is [mlt'], extracted after reduction *)
-		      (* The shortest is [mlt], which use abbreviations *)
-		      (* If possible, we take [mlt], otherwise [mlt']. *)
-		      if eq_ml_type (expand env mlt) (expand env mlt') then mlt else mlt')
-	   | (Info, Default) ->
+                      (* ML type abbreviations interact badly with Coq *)
+                      (* reduction, so [mlt] and [mlt'] might be different: *)
+                      (* The more precise is [mlt'], extracted after reduction *)
+                      (* The shortest is [mlt], which use abbreviations *)
+                      (* If possible, we take [mlt], otherwise [mlt']. *)
+                      if eq_ml_type (expand env mlt) (expand env mlt') then mlt else mlt')
+           | (Info, Default) ->
                (* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
                (match (lookup_constant kn env).const_body with
                  | Undef _  | OpaqueDef _ | Primitive _ -> Tunknown (* Brutal approx ... *)
-		  | Def lbody ->
-		      (* We try to reduce. *)
+                  | Def lbody ->
+                      (* We try to reduce. *)
                       let newc = applistc (get_body lbody) args in
                       extract_type env sg db j newc []))
     | Ind ((kn,i),u) ->
@@ -415,15 +415,15 @@ and extract_really_ind env kn mib =
        (cf Vector and bug #2570) *)
     let equiv =
       if lang () != Ocaml ||
-	 (not (modular ()) && at_toplevel (MutInd.modpath kn)) ||
-	 KerName.equal (MutInd.canonical kn) (MutInd.user kn)
+         (not (modular ()) && at_toplevel (MutInd.modpath kn)) ||
+         KerName.equal (MutInd.canonical kn) (MutInd.user kn)
       then
-	NoEquiv
+        NoEquiv
       else
-	begin
-	  ignore (extract_ind env (MutInd.make1 (MutInd.canonical kn)));
-	  Equiv (MutInd.canonical kn)
-	end
+        begin
+          ignore (extract_ind env (MutInd.make1 (MutInd.canonical kn)));
+          Equiv (MutInd.canonical kn)
+        end
     in
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
@@ -435,20 +435,20 @@ and extract_really_ind env kn mib =
     (* their type var list. *)
     let packets =
       Array.mapi
-	(fun i mip ->
+        (fun i mip ->
            let (_,u),_ = UnivGen.fresh_inductive_instance env (kn,i) in
-	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
+           let ar = Inductive.type_of_inductive env ((mib,mip),u) in
            let ar = EConstr.of_constr ar in
            let info = (fst (flag_of_type env sg ar) = Info) in
            let s,v = if info then type_sign_vl env sg ar else [],[] in
-	   let t = Array.make (Array.length mip.mind_nf_lc) [] in
-	   { ip_typename = mip.mind_typename;
-	     ip_consnames = mip.mind_consnames;
-	     ip_logical = not info;
-	     ip_sign = s;
-	     ip_vars = v;
-	     ip_types = t }, u)
-	mib.mind_packets
+           let t = Array.make (Array.length mip.mind_nf_lc) [] in
+           { ip_typename = mip.mind_typename;
+             ip_consnames = mip.mind_consnames;
+             ip_logical = not info;
+             ip_sign = s;
+             ip_vars = v;
+             ip_types = t }, u)
+        mib.mind_packets
     in
 
     add_ind kn mib
@@ -461,85 +461,85 @@ and extract_really_ind env kn mib =
     for i = 0 to mib.mind_ntypes - 1 do
       let p,u = packets.(i) in
       if not p.ip_logical then
-	let types = arities_of_constructors env ((kn,i),u) in
-	for j = 0 to Array.length types - 1 do
-	  let t = snd (decompose_prod_n npar types.(j)) in
-	  let prods,head = dest_prod epar t in
-	  let nprods = List.length prods in
+        let types = arities_of_constructors env ((kn,i),u) in
+        for j = 0 to Array.length types - 1 do
+          let t = snd (decompose_prod_n npar types.(j)) in
+          let prods,head = dest_prod epar t in
+          let nprods = List.length prods in
           let args = match Constr.kind head with
             | App (f,args) -> args (* [Constr.kind f = Ind ip] *)
             | _ -> [||]
           in
-	  let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
-	  let db = db_from_ind dbmap npar in
+          let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
+          let db = db_from_ind dbmap npar in
           p.ip_types.(j) <-
             extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1)
-	done
+        done
     done;
     (* Third pass: we determine special cases. *)
     let ind_info =
       try
-	let ip = (kn, 0) in
+        let ip = (kn, 0) in
         let r = GlobRef.IndRef ip in
-	if is_custom r then raise (I Standard);
+        if is_custom r then raise (I Standard);
         if mib.mind_finite == CoFinite then raise (I Coinductive);
-	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
-	let p,u = packets.(0) in
-	if p.ip_logical then raise (I Standard);
-	if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard);
-	let typ = p.ip_types.(0) in
-	let l = List.filter (fun t -> not (isTdummy (expand env t))) typ in
-	if not (keep_singleton ()) &&
-	    Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
-	then raise (I Singleton);
-	if List.is_empty l then raise (I Standard);
+        if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
+        let p,u = packets.(0) in
+        if p.ip_logical then raise (I Standard);
+        if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard);
+        let typ = p.ip_types.(0) in
+        let l = List.filter (fun t -> not (isTdummy (expand env t))) typ in
+        if not (keep_singleton ()) &&
+            Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
+        then raise (I Singleton);
+        if List.is_empty l then raise (I Standard);
         if mib.mind_record == Declarations.NotRecord then raise (I Standard);
-	(* Now we're sure it's a record. *)
-	(* First, we find its field names. *)
-	let rec names_prod t = match Constr.kind t with
+        (* Now we're sure it's a record. *)
+        (* First, we find its field names. *)
+        let rec names_prod t = match Constr.kind t with
           | Prod(n,_,t) -> n::(names_prod t)
           | LetIn(_,_,_,t) -> names_prod t
-	  | Cast(t,_,_) -> names_prod t
-	  | _ -> []
-	in
-	let field_names =
-	  List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
-	assert (Int.equal (List.length field_names) (List.length typ));
-	let projs = ref Cset.empty in
-	let mp = MutInd.modpath kn in
-	let rec select_fields l typs = match l,typs with
-	  | [],[] -> []
-	  | _::l, typ::typs when isTdummy (expand env typ) ->
-	      select_fields l typs
+          | Cast(t,_,_) -> names_prod t
+          | _ -> []
+        in
+        let field_names =
+          List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
+        assert (Int.equal (List.length field_names) (List.length typ));
+        let projs = ref Cset.empty in
+        let mp = MutInd.modpath kn in
+        let rec select_fields l typs = match l,typs with
+          | [],[] -> []
+          | _::l, typ::typs when isTdummy (expand env typ) ->
+              select_fields l typs
           | {binder_name=Anonymous}::l, typ::typs ->
-	      None :: (select_fields l typs)
+              None :: (select_fields l typs)
           | {binder_name=Name id}::l, typ::typs ->
-	      let knp = Constant.make2 mp (Label.of_id id) in
-	      (* Is it safe to use [id] for projections [foo.id] ? *)
-	      if List.for_all ((==) Keep) (type2signature env typ)
-	      then projs := Cset.add knp !projs;
+              let knp = Constant.make2 mp (Label.of_id id) in
+              (* Is it safe to use [id] for projections [foo.id] ? *)
+              if List.for_all ((==) Keep) (type2signature env typ)
+              then projs := Cset.add knp !projs;
               Some (GlobRef.ConstRef knp) :: (select_fields l typs)
-	  | _ -> assert false
-	in
-	let field_glob = select_fields field_names typ
-	in
-	(* Is this record officially declared with its projections ? *)
-	(* If so, we use this information. *)
-	begin try
+          | _ -> assert false
+        in
+        let field_glob = select_fields field_names typ
+        in
+        (* Is this record officially declared with its projections ? *)
+        (* If so, we use this information. *)
+        begin try
           let ty = Inductive.type_of_inductive env ((mib,mip0),u) in
           let n = nb_default_params env sg (EConstr.of_constr ty) in
           let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
           in
-	  List.iter (Option.iter check_proj) (lookup_projections ip)
-	with Not_found -> ()
-	end;
-	Record field_glob
+          List.iter (Option.iter check_proj) (lookup_projections ip)
+        with Not_found -> ()
+        end;
+        Record field_glob
       with (I info) -> info
     in
     let i = {ind_kind = ind_info;
-	     ind_nparams = npar;
-	     ind_packets = Array.map fst packets;
-	     ind_equiv = equiv }
+             ind_nparams = npar;
+             ind_packets = Array.map fst packets;
+             ind_equiv = equiv }
     in
     add_ind kn mib i;
     add_inductive_kind kn i.ind_kind;
@@ -622,42 +622,42 @@ let rec extract_term env sg mle mlt c args =
     | Lambda (n, t, d) ->
       let id = map_annot id_of_name n in
       let idna = map_annot Name.mk_name id in
-	(match args with
-	   | a :: l ->
-	       (* We make as many [LetIn] as possible. *)
+        (match args with
+           | a :: l ->
+               (* We make as many [LetIn] as possible. *)
                let l' = List.map (EConstr.Vars.lift 1) l in
                let d' = EConstr.mkLetIn (idna,a,t,applistc d l') in
                extract_term env sg mle mlt d' []
            | [] ->
                let env' = push_rel_assum (idna, t) env in
-	       let id, a =
+               let id, a =
                  try check_default env sg t; Id id.binder_name, new_meta()
                  with NotDefault d -> Dummy, Tdummy d
-	       in
-	       let b = new_meta () in
-	       (* If [mlt] cannot be unified with an arrow type, then magic! *)
-	       let magic = needs_magic (mlt, Tarr (a, b)) in
+               in
+               let b = new_meta () in
+               (* If [mlt] cannot be unified with an arrow type, then magic! *)
+               let magic = needs_magic (mlt, Tarr (a, b)) in
                let d' = extract_term env' sg (Mlenv.push_type mle a) b d [] in
-	       put_magic_if magic (MLlam (id, d')))
+               put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
         let id = map_annot id_of_name n in
         let env' = EConstr.push_rel (LocalDef (map_annot Name.mk_name id, c1, t1)) env in
         (* We directly push the args inside the [LetIn].
            TODO: the opt_let_app flag is supposed to prevent that *)
         let args' = List.map (EConstr.Vars.lift 1) args in
-	(try
+        (try
           check_default env sg t1;
-	  let a = new_meta () in
+          let a = new_meta () in
           let c1' = extract_term env sg mle a c1 [] in
-	  (* The type of [c1'] is generalized and stored in [mle]. *)
-	  let mle' =
-	    if generalizable c1'
-	    then Mlenv.push_gen mle a
-	    else Mlenv.push_type mle a
-	  in
+          (* The type of [c1'] is generalized and stored in [mle]. *)
+          let mle' =
+            if generalizable c1'
+            then Mlenv.push_gen mle a
+            else Mlenv.push_type mle a
+          in
           MLletin (Id id.binder_name, c1', extract_term env' sg mle' mlt c2 args')
-	with NotDefault d ->
-	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
+        with NotDefault d ->
+          let mle' = Mlenv.push_std_type mle (Tdummy d) in
           ast_pop (extract_term env' sg mle' mlt c2 args'))
     | Const (kn,_) ->
         extract_cst_app env sg mle mlt kn args
@@ -667,9 +667,9 @@ let rec extract_term env sg mle mlt c args =
         let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
         extract_term env sg mle mlt term args
     | Rel n ->
-	(* As soon as the expected [mlt] for the head is known, *)
-	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
-	let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
+        (* As soon as the expected [mlt] for the head is known, *)
+        (* we unify it with an fresh copy of the stored type of [Rel n]. *)
+        let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
         in extract_app env sg mle mlt extract_rel args
     | Case ({ci_ind=ip},_,c0,br) ->
         extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
@@ -816,8 +816,8 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args =
       put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
     else
       let typeargs = match snd (type_decomp type_cons) with
-	| Tglob (_,l) -> List.map type_simpl l
-	| _ -> assert false
+        | Tglob (_,l) -> List.map type_simpl l
+        | _ -> assert false
       in
       let typ = Tglob(GlobRef.IndRef ip, typeargs) in
       put_magic_if magic1 (MLcons (typ, GlobRef.ConstructRef cp, mla))
@@ -854,14 +854,14 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
     (* The only non-informative case: [c] is of sort [Prop] *)
     if (sort_of env sg t) == InProp then
       begin
-	add_recursors env kn; (* May have passed unseen if logical ... *)
-	(* Logical singleton case: *)
-	(* [match c with C i j k -> t] becomes [t'] *)
-	assert (Int.equal br_size 1);
-	let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in
-	let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in
+        add_recursors env kn; (* May have passed unseen if logical ... *)
+        (* Logical singleton case: *)
+        (* [match c with C i j k -> t] becomes [t'] *)
+        assert (Int.equal br_size 1);
+        let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in
+        let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in
         let e = extract_maybe_term env sg mle mlt br.(0) in
-	snd (case_expunge s e)
+        snd (case_expunge s e)
       end
     else
       let mi = extract_ind env kn in
@@ -873,32 +873,32 @@ and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
       (* The extraction of each branch. *)
       let extract_branch i =
         let r = GlobRef.ConstructRef (ip,i+1) in
-	(* The types of the arguments of the corresponding constructor. *)
-	let f t = type_subst_vect metas (expand env t) in
-	let l = List.map f oi.ip_types.(i) in
-	(* the corresponding signature *)
-	let s = List.map (type2sign env) oi.ip_types.(i) in
-	let s = sign_with_implicits r s mi.ind_nparams in
-	(* Extraction of the branch (in functional form). *)
+        (* The types of the arguments of the corresponding constructor. *)
+        let f t = type_subst_vect metas (expand env t) in
+        let l = List.map f oi.ip_types.(i) in
+        (* the corresponding signature *)
+        let s = List.map (type2sign env) oi.ip_types.(i) in
+        let s = sign_with_implicits r s mi.ind_nparams in
+        (* Extraction of the branch (in functional form). *)
         let e = extract_maybe_term env sg mle (type_recomp (l,mlt)) br.(i) in
-	(* We suppress dummy arguments according to signature. *)
-	let ids,e = case_expunge s e in
-	(List.rev ids, Pusual r, e)
+        (* We suppress dummy arguments according to signature. *)
+        let ids,e = case_expunge s e in
+        (List.rev ids, Pusual r, e)
       in
       if mi.ind_kind == Singleton then
-	begin
-	  (* Informative singleton case: *)
-	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
-	  assert (Int.equal br_size 1);
-	  let (ids,_,e') = extract_branch 0 in
-	  assert (Int.equal (List.length ids) 1);
-	  MLletin (tmp_id (List.hd ids),a,e')
-	end
+        begin
+          (* Informative singleton case: *)
+          (* [match c with C i -> t] becomes [let i = c' in t'] *)
+          assert (Int.equal br_size 1);
+          let (ids,_,e') = extract_branch 0 in
+          assert (Int.equal (List.length ids) 1);
+          MLletin (tmp_id (List.hd ids),a,e')
+        end
       else
-	(* Standard case: we apply [extract_branch]. *)
-	let typs = List.map type_simpl (Array.to_list metas) in
+        (* Standard case: we apply [extract_branch]. *)
+        let typs = List.map type_simpl (Array.to_list metas) in
         let typ = Tglob (GlobRef.IndRef ip,typs) in
-	MLcase (typ, a, Array.init br_size extract_branch)
+        MLcase (typ, a, Array.init br_size extract_branch)
 
 (*s Extraction of a (co)-fixpoint. *)
 
@@ -932,7 +932,7 @@ let rec gentypvar_ok sg c = match EConstr.kind sg c with
   | Lambda _ | Const _ -> true
   | App (c,v) ->
       (* if all arguments are variables, these variables will
-	 disappear after extraction (see [empty_s] below) *)
+         disappear after extraction (see [empty_s] below) *)
       Array.for_all (EConstr.isRel sg) v && gentypvar_ok sg c
   | Cast (c,_,_) -> gentypvar_ok sg c
   | _ -> false
@@ -962,7 +962,7 @@ let extract_std_constant env sg kn body typ =
     else
       let s,s' = List.chop m s in
       if List.for_all ((==) Keep) s' &&
-	(lang () == Haskell || sign_kind s != UnsafeLogicalSig)
+        (lang () == Haskell || sign_kind s != UnsafeLogicalSig)
       then decompose_lam_n sg m body
       else decomp_lams_eta_n n m env sg body typ
   in
@@ -1114,27 +1114,27 @@ let extract_constant env kn cb =
     | (Info,TypeScheme) ->
         (match cb.const_body with
           | Primitive _ | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c ->
+          | Def c ->
              (match Recordops.find_primitive_projection kn with
               | None -> mk_typ (get_body c)
               | Some p ->
                 let body = fake_match_projection env p in
                 mk_typ (EConstr.of_constr body))
-	  | OpaqueDef c ->
-	    add_opaque r;
+          | OpaqueDef c ->
+            add_opaque r;
             if access_opaque () then mk_typ (get_opaque env c)
             else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
           | Primitive _ | Undef _ -> warn_info (); mk_ax ()
-	  | Def c ->
+          | Def c ->
              (match Recordops.find_primitive_projection kn with
               | None -> mk_def (get_body c)
               | Some p ->
                 let body = fake_match_projection env p in
                 mk_def (EConstr.of_constr body))
-	  | OpaqueDef c ->
-	    add_opaque r;
+          | OpaqueDef c ->
+            add_opaque r;
             if access_opaque () then mk_def (get_opaque env c)
             else mk_ax ())
   with SingletonInductiveBecomesProp id ->
@@ -1150,10 +1150,10 @@ let extract_constant_spec env kn cb =
     | (Logic, Default) -> Sval (r, Tdummy Kprop)
     | (Info, TypeScheme) ->
         let s,vl = type_sign_vl env sg typ in
-	(match cb.const_body with
+        (match cb.const_body with
           | Undef _ | OpaqueDef _ | Primitive _ -> Stype (r, vl, None)
-	  | Def body ->
-	      let db = db_from_sign s in
+          | Def body ->
+              let db = db_from_sign s in
               let body = get_body body in
               let t = extract_type_scheme env sg db body (List.length s)
               in Stype (r, vl, Some t))
@@ -1197,9 +1197,9 @@ let extract_inductive env kn =
     let rec filter i = function
       | [] -> []
       | t::l ->
-	  let l' = filter (succ i) l in
-	  if isTdummy (expand env t) || Int.Set.mem i implicits then l'
-	  else t::l'
+          let l' = filter (succ i) l in
+          if isTdummy (expand env t) || Int.Set.mem i implicits then l'
+          else t::l'
     in filter (1+ind.ind_nparams) l
   in
   let packets =
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 4769bef475..f0053ba6b5 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -110,15 +110,15 @@ let rec pp_type par vl t =
        with Failure _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (GlobRef.IndRef(kn,0),l)
-	when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
-	  pp_type true vl (List.hd l)
+        when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
+          pp_type true vl (List.hd l)
     | Tglob (r,l) ->
-	  pp_par par
-	    (pp_global Type r ++ spc () ++
-	     prlist_with_sep spc (pp_type true vl) l)
+          pp_par par
+            (pp_global Type r ++ spc () ++
+             prlist_with_sep spc (pp_type true vl) l)
     | Tarr (t1,t2) ->
-	pp_par par
-	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
+        pp_par par
+          (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy _ -> str "()"
     | Tunknown -> str "Any"
     | Taxiom -> str "() -- AXIOM TO BE REALIZED" ++ fnl ()
@@ -141,77 +141,77 @@ let rec pp_expr par env args =
   and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
-	let id = get_db_name n env in
+        let id = get_db_name n env in
         (* Try to survive to the occurrence of a Dummy rel.
            TODO: we should get rid of this hack (cf. BZ#592) *)
         let id = if Id.equal id dummy_name then Id.of_string "__" else id in
         apply (Id.print id)
     | MLapp (f,args') ->
-	let stl = List.map (pp_expr true env []) args' in
+        let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
     | MLlam _ as a ->
-      	let fl,a' = collect_lams a in
-	let fl,env' = push_vars (List.map id_of_mlid fl) env in
-	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
-	apply2 st
+        let fl,a' = collect_lams a in
+        let fl,env' = push_vars (List.map id_of_mlid fl) env in
+        let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
+        apply2 st
     | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id_of_mlid id] env in
-	let pp_id = Id.print (List.hd i)
-	and pp_a1 = pp_expr false env [] a1
-	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
-	let pp_def =
-	  str "let {" ++ cut () ++
-	  hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}")
-	in
-	apply2 (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
-		       spc () ++ hov 0 pp_a2))
+        let i,env' = push_vars [id_of_mlid id] env in
+        let pp_id = Id.print (List.hd i)
+        and pp_a1 = pp_expr false env [] a1
+        and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
+        let pp_def =
+          str "let {" ++ cut () ++
+          hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}")
+        in
+        apply2 (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
+                       spc () ++ hov 0 pp_a2))
     | MLglob r ->
-	apply (pp_global Term r)
+        apply (pp_global Term r)
     | MLcons (_,r,a) as c ->
         assert (List.is_empty args);
         begin match a with
-	  | _ when is_native_char c -> pp_native_char c
-	  | [] -> pp_global Cons r
-	  | [a] ->
-	    pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
-	  | _ ->
-	    pp_par par (pp_global Cons r ++ spc () ++
-			prlist_with_sep spc (pp_expr true env []) a)
-	end
+          | _ when is_native_char c -> pp_native_char c
+          | [] -> pp_global Cons r
+          | [a] ->
+            pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
+          | _ ->
+            pp_par par (pp_global Cons r ++ spc () ++
+                        prlist_with_sep spc (pp_expr true env []) a)
+        end
     | MLtuple l ->
         assert (List.is_empty args);
         pp_boxed_tuple (pp_expr true env []) l
     | MLcase (_,t, pv) when is_custom_match pv ->
         if not (is_regular_match pv) then
-	  user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
-	let mkfun (ids,_,e) =
-	  if not (List.is_empty ids) then named_lams (List.rev ids) e
-	  else dummy_lams (ast_lift 1 e) 1
-	in
-	let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
-	let inner =
-	  str (find_custom_match pv) ++ fnl () ++
-	  prvect pp_branch pv ++
-	  pp_expr true env [] t
-	in
-	apply2 (hov 2 inner)
+          user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
+        let mkfun (ids,_,e) =
+          if not (List.is_empty ids) then named_lams (List.rev ids) e
+          else dummy_lams (ast_lift 1 e) 1
+        in
+        let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
+        let inner =
+          str (find_custom_match pv) ++ fnl () ++
+          prvect pp_branch pv ++
+          pp_expr true env [] t
+        in
+        apply2 (hov 2 inner)
     | MLcase (typ,t,pv) ->
         apply2
-	  (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
-		fnl () ++ pp_pat env pv))
+          (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
+                fnl () ++ pp_pat env pv))
     | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
+        let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+        pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s ->
-	(* An [MLexn] may be applied, but I don't really care. *)
-	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
+        (* An [MLexn] may be applied, but I don't really care. *)
+        pp_par par (str "Prelude.error" ++ spc () ++ qs s)
     | MLdummy k ->
         (* An [MLdummy] may be applied, but I don't really care. *)
         (match msg_of_implicit k with
          | "" -> str "__"
          | s -> str "__" ++ spc () ++ pp_bracket_comment (str s))
     | MLmagic a ->
-	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
+        pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
     | MLuint _ ->
       pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
@@ -232,16 +232,16 @@ and pp_gen_pat par ids env = function
 and pp_one_pat env (ids,p,t) =
   let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in
   hov 2 (str " " ++
-	 pp_gen_pat false (List.rev ids') env' p ++
-	 str " ->" ++ spc () ++
-	 pp_expr (expr_needs_par t) env' [] t)
+         pp_gen_pat false (List.rev ids') env' p ++
+         str " ->" ++ spc () ++
+         pp_expr (expr_needs_par t) env' [] t)
 
 and pp_pat env pv =
   prvecti
     (fun i x ->
        pp_one_pat env pv.(i) ++
        if Int.equal i (Array.length pv - 1) then str "}" else
-	 (str ";" ++ fnl ()))
+         (str ";" ++ fnl ()))
     pv
 
 (*s names of the functions ([ids]) are already pushed in [env],
@@ -251,10 +251,10 @@ and pp_fix par env i (ids,bl) args =
   pp_par par
     (v 0
        (v 1 (str "let {" ++ fnl () ++
-	     prvect_with_sep (fun () -> str ";" ++ fnl ())
-	       (fun (fi,ti) -> pp_function env (Id.print fi) ti)
-	       (Array.map2 (fun a b -> a,b) ids bl) ++
-	     str "}") ++
+             prvect_with_sep (fun () -> str ";" ++ fnl ())
+               (fun (fi,ti) -> pp_function env (Id.print fi) ti)
+               (Array.map2 (fun a b -> a,b) ids bl) ++
+             str "}") ++
         fnl () ++ str "in " ++ pp_apply (Id.print ids.(i)) false args))
 
 and pp_function env f t =
@@ -269,17 +269,17 @@ and pp_function env f t =
 let pp_logical_ind packet =
   pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
   pp_comment (str "with constructors : " ++
-	      prvect_with_sep spc Id.print packet.ip_consnames)
+              prvect_with_sep spc Id.print packet.ip_consnames)
 
 let pp_singleton kn packet =
   let name = pp_global Type (GlobRef.IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ name ++ spc () ++
-	 prlist_with_sep spc Id.print l ++
-	 (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
-	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment (str "singleton inductive, whose constructor was " ++
-		     Id.print packet.ip_consnames.(0)))
+         prlist_with_sep spc Id.print l ++
+         (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
+         pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
+         pp_comment (str "singleton inductive, whose constructor was " ++
+                     Id.print packet.ip_consnames.(0)))
 
 let pp_one_ind ip pl cv =
   let pl = rename_tvars keywords pl in
@@ -288,8 +288,8 @@ let pp_one_ind ip pl cv =
      match l with
        | [] -> (mt ())
        | _  -> (str " " ++
-      	       	prlist_with_sep
-		  (fun () -> (str " ")) (pp_type true pl) l))
+                prlist_with_sep
+                  (fun () -> (str " ")) (pp_type true pl) l))
   in
   str (if Array.is_empty cv then "type " else "data ") ++
   pp_global Type (GlobRef.IndRef ip) ++
@@ -298,7 +298,7 @@ let pp_one_ind ip pl cv =
   else
     (fnl () ++ str " " ++
      v 0 (str "  " ++
-	  prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor
+          prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor
             (Array.mapi (fun i c -> GlobRef.ConstructRef (ip,i+1),c) cv)))
 
 let rec pp_ind first kn i ind =
@@ -310,10 +310,10 @@ let rec pp_ind first kn i ind =
     if is_custom (GlobRef.IndRef (kn,i)) then pp_ind first kn (i+1) ind
     else
       if p.ip_logical then
-	pp_logical_ind p ++ pp_ind first kn (i+1) ind
+        pp_logical_ind p ++ pp_ind first kn (i+1) ind
       else
-	pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++
-	pp_ind false kn (i+1) ind
+        pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++
+        pp_ind false kn (i+1) ind
 
 
 (*s Pretty-printing of a declaration. *)
@@ -325,45 +325,45 @@ let pp_decl = function
   | Dtype (r, l, t) ->
       if is_inline_custom r then mt ()
       else
-	let l = rename_tvars keywords l in
-	let st =
-	  try
-	    let ids,s = find_type_custom r in
-	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
-	  with Not_found ->
-	    prlist (fun id -> Id.print id ++ str " ") l ++
-	    if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl ()
-	    else str "=" ++ spc () ++ pp_type false l t
-	in
-	hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
+        let l = rename_tvars keywords l in
+        let st =
+          try
+            let ids,s = find_type_custom r in
+            prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
+          with Not_found ->
+            prlist (fun id -> Id.print id ++ str " ") l ++
+            if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl ()
+            else str "=" ++ spc () ++ pp_type false l t
+        in
+        hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
   | Dfix (rv, defs, typs) ->
       let names = Array.map
-	(fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+        (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
       in
       prvecti
-	(fun i r ->
-	  let void = is_inline_custom r ||
-	    (not (is_custom r) &&
+        (fun i r ->
+          let void = is_inline_custom r ||
+            (not (is_custom r) &&
              match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
-	  in
-	  if void then mt ()
-	  else
-	    hov 2 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++
-	    (if is_custom r then
-		(names.(i) ++ str " = " ++ str (find_custom r))
-	     else
-		(pp_function (empty_env ()) names.(i) defs.(i)))
-	    ++ fnl2 ())
-	rv
+          in
+          if void then mt ()
+          else
+            hov 2 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++
+            (if is_custom r then
+                (names.(i) ++ str " = " ++ str (find_custom r))
+             else
+                (pp_function (empty_env ()) names.(i) defs.(i)))
+            ++ fnl2 ())
+        rv
   | Dterm (r, a, t) ->
       if is_inline_custom r then mt ()
       else
-	let e = pp_global Term r in
-	hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++
-	  if is_custom r then
-	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
-	  else
-	    hov 0 (pp_function (empty_env ()) e a ++ fnl2 ())
+        let e = pp_global Term r in
+        hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++
+          if is_custom r then
+            hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
+          else
+            hov 0 (pp_function (empty_env ()) e a ++ fnl2 ())
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 44b95ae4c1..fc0ba95b98 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -200,10 +200,10 @@ module Mlenv = struct
     let rec meta2var t = match t with
       | Tmeta {contents=Some u} -> meta2var u
       | Tmeta ({id=i} as m) ->
-	  (try Tvar (Int.Map.find i !map)
-	   with Not_found ->
-	     if Metaset.mem m mle.free then t
-	     else Tvar (add_new i))
+          (try Tvar (Int.Map.find i !map)
+           with Not_found ->
+             if Metaset.mem m mle.free then t
+             else Tvar (add_new i))
       | Tarr (t1,t2) -> Tarr (meta2var t1, meta2var t2)
       | Tglob (r,l) -> Tglob (r, List.map meta2var l)
       | t -> t
@@ -279,9 +279,9 @@ let type_expand env t =
   let rec expand = function
     | Tmeta {contents = Some t} -> expand t
     | Tglob (r,l) ->
-	(match env r with
-	   | Some mlt -> expand (type_subst_list l mlt)
-	   | None -> Tglob (r, List.map expand l))
+        (match env r with
+           | Some mlt -> expand (type_subst_list l mlt)
+           | None -> Tglob (r, List.map expand l))
     | Tarr (a,b) -> Tarr (expand a, expand b)
     | a -> a
   in if Table.type_expand () then expand t else t
@@ -348,8 +348,8 @@ let type_expunge_from_sign env s t =
     | _, Tmeta {contents = Some t} -> expunge s t
     | _, Tglob (r,l) ->
        (match env r with
-	| Some mlt -> expunge s (type_subst_list l mlt)
-	| None -> assert false)
+        | Some mlt -> expunge s (type_subst_list l mlt)
+        | None -> assert false)
     | _ -> assert false
   in
   let t = expunge (sign_no_final_keeps s) t in
@@ -426,7 +426,7 @@ let ast_iter_rel f =
     | MLlam (_,a) -> iter (n+1) a
     | MLletin (_,a,b) -> iter n a; iter (n+1) b
     | MLcase (_,a,v) ->
-	iter n a; Array.iter (fun (l,_,t) -> iter (n + (List.length l)) t) v
+        iter n a; Array.iter (fun (l,_,t) -> iter (n + (List.length l)) t) v
     | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
     | MLcons (_,_,l) | MLtuple l ->  List.iter (iter n) l
@@ -512,8 +512,8 @@ let nb_occur_match =
     | MLrel i -> if Int.equal i k then 1 else 0
     | MLcase(_,a,v) ->
         (nb k a) +
-	Array.fold_left
-	  (fun r (ids,_,a) -> max r (nb (k+(List.length ids)) a)) 0 v
+        Array.fold_left
+          (fun r (ids,_,a) -> max r (nb (k+(List.length ids)) a)) 0 v
     | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b)
     | MLfix (_,ids,v) -> let k = k+(Array.length ids) in
       Array.fold_left (fun r a -> r+(nb k a)) 0 v
@@ -605,10 +605,10 @@ let ast_pop t = ast_lift (-1) t
 let permut_rels k k' =
   let rec permut n = function
     | MLrel i as a ->
-	let i' = i-n in
-	if i'<1 || i'>k+k' then a
-	else if i'<=k then MLrel (i+k')
-	else MLrel (i-k)
+        let i' = i-n in
+        if i'<1 || i'>k+k' then a
+        else if i'<=k then MLrel (i+k')
+        else MLrel (i-k)
     | a -> ast_map_lift permut n a
   in permut 0
 
@@ -618,10 +618,10 @@ let permut_rels k k' =
 let ast_subst e =
   let rec subst n = function
     | MLrel i as a ->
-	let i' = i-n in
-	if Int.equal i' 1 then ast_lift n e
-	else if i'<1 then a
-	else MLrel (i-1)
+        let i' = i-n in
+        if Int.equal i' 1 then ast_lift n e
+        else if i'<1 then a
+        else MLrel (i-1)
     | a -> ast_map_lift subst n a
   in subst 0
 
@@ -633,13 +633,13 @@ let ast_subst e =
 let gen_subst v d t =
   let rec subst n = function
     | MLrel i as a ->
-	let i'= i-n in
-	if i' < 1 then a
-	else if i' <= Array.length v then
-	  match v.(i'-1) with
-	    | None -> assert false
-	    | Some u -> ast_lift n u
-	else MLrel (i+d)
+        let i'= i-n in
+        if i' < 1 then a
+        else if i' <= Array.length v then
+          match v.(i'-1) with
+            | None -> assert false
+            | Some u -> ast_lift n u
+        else MLrel (i+d)
     | a -> ast_map_lift subst n a
   in subst 0 t
 
@@ -661,18 +661,18 @@ let is_regular_match br =
   else
     try
       let get_r (ids,pat,c) =
-	match pat with
-	  | Pusual r -> r
-	  | Pcons (r,l) ->
+        match pat with
+          | Pusual r -> r
+          | Pcons (r,l) ->
             let is_rel i = function Prel j -> Int.equal i j | _ -> false in
-	    if not (List.for_all_i is_rel 1 (List.rev l))
-	    then raise Impossible;
-	    r
-	  | _ -> raise Impossible
+            if not (List.for_all_i is_rel 1 (List.rev l))
+            then raise Impossible;
+            r
+          | _ -> raise Impossible
       in
       let ind = match get_r br.(0) with
         | GlobRef.ConstructRef (ind,_) -> ind
-	| _ -> raise Impossible
+        | _ -> raise Impossible
       in
       let is_ref i tr = match get_r tr with
       | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
@@ -767,20 +767,20 @@ let eta_red e =
   if Int.equal n 0 then e
   else match t with
     | MLapp (f,a) ->
-	let m = List.length a in
-	let ids,body,args =
-	  if Int.equal m n then
-	    [], f, a
-	  else if m < n then
-	    List.skipn m ids, f, a
-	  else (* m > n *)
-	    let a1,a2 = List.chop (m-n) a in
-	    [], MLapp (f,a1), a2
-	in
-	let p = List.length args in
-	if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body)
-	then named_lams ids (ast_lift (-p) body)
-	else e
+        let m = List.length a in
+        let ids,body,args =
+          if Int.equal m n then
+            [], f, a
+          else if m < n then
+            List.skipn m ids, f, a
+          else (* m > n *)
+            let a1,a2 = List.chop (m-n) a in
+            [], MLapp (f,a1), a2
+        in
+        let p = List.length args in
+        if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body)
+        then named_lams ids (ast_lift (-p) body)
+        else e
     | _ -> e
 
 (* Performs an eta-reduction when the core is atomic and value,
@@ -804,11 +804,11 @@ let rec linear_beta_red a t = match a,t with
   | [], _ -> t
   | a0::a, MLlam (id,t) ->
       (match nb_occur_match t with
-	 | 0 -> linear_beta_red a (ast_pop t)
-	 | 1 -> linear_beta_red a (ast_subst a0 t)
-	 | _ ->
-	     let a = List.map (ast_lift 1) a in
-	     MLletin (id, a0, linear_beta_red a t))
+         | 0 -> linear_beta_red a (ast_pop t)
+         | 1 -> linear_beta_red a (ast_subst a0 t)
+         | _ ->
+             let a = List.map (ast_lift 1) a in
+             MLletin (id, a0, linear_beta_red a t))
   | _ -> MLapp (t, a)
 
 let rec tmp_head_lams = function
@@ -860,10 +860,10 @@ let branch_as_fun typ (l,p,c) =
   in
   let rec genrec n = function
     | MLrel i as c ->
-	let i' = i-n in
-	if i'<1 then c
-	else if i'>nargs then MLrel (i-nargs+1)
-	else raise Impossible
+        let i' = i-n in
+        if i'<1 then c
+        else if i'>nargs then MLrel (i-nargs+1)
+        else raise Impossible
     | MLcons _ as cons' when eq_ml_ast cons' (ast_lift n cons) -> MLrel (n+1)
     | a -> ast_map_lift genrec n a
   in genrec 0 c
@@ -909,8 +909,8 @@ let census_add, census_max, census_clean =
     let len = ref 0 and lst = ref Int.Set.empty and elm = ref MLaxiom in
     List.iter
       (fun (e, s) ->
-	 let n = Int.Set.cardinal s in
-	 if n > !len then begin len := n; lst := s; elm := e end)
+         let n = Int.Set.cardinal s in
+         if n > !len then begin len := n; lst := s; elm := e end)
       !h;
     (!elm,!lst)
   in
@@ -931,9 +931,9 @@ let factor_branches o typ br =
     census_clean ();
     for i = 0 to Array.length br - 1 do
       if o.opt_case_idr then
-	(try census_add (branch_as_fun typ br.(i)) i with Impossible -> ());
+        (try census_add (branch_as_fun typ br.(i)) i with Impossible -> ());
       if o.opt_case_cst then
-	(try census_add (branch_as_cst br.(i)) i with Impossible -> ());
+        (try census_add (branch_as_cst br.(i)) i with Impossible -> ());
     done;
     let br_factor, br_set = census_max () in
     census_clean ();
@@ -956,9 +956,9 @@ let is_exn = function MLexn _ -> true | _ -> false
 let permut_case_fun br acc =
   let nb = ref max_int in
   Array.iter (fun (_,_,t) ->
-		let ids, c = collect_lams t in
-		let n = List.length ids in
-		if (n < !nb) && (not (is_exn c)) then nb := n) br;
+                let ids, c = collect_lams t in
+                let n = List.length ids in
+                if (n < !nb) && (not (is_exn c)) then nb := n) br;
   if Int.equal !nb  max_int || Int.equal !nb 0 then ([],br)
   else begin
     let br = Array.copy br in
@@ -967,11 +967,11 @@ let permut_case_fun br acc =
       let (l,p,t) = br.(i) in
       let local_nb = nb_lams t in
       if local_nb < !nb then (* t = MLexn ... *)
-	br.(i) <- (l,p,remove_n_lams local_nb t)
+        br.(i) <- (l,p,remove_n_lams local_nb t)
       else begin
-	let local_ids,t = collect_n_lams !nb t in
-	ids := merge_ids !ids local_ids;
-	br.(i) <- (l,p,permut_rels !nb (List.length l) t)
+        let local_ids,t = collect_n_lams !nb t in
+        ids := merge_ids !ids local_ids;
+        br.(i) <- (l,p,permut_rels !nb (List.length l) t)
       end
     done;
     (!ids,br)
@@ -1011,9 +1011,9 @@ let iota_gen br hd =
   let rec iota k = function
     | MLcons (typ,r,a) -> iota_red 0 k br (typ,r,a)
     | MLcase(typ,e,br') ->
-	let new_br =
-	  Array.map (fun (i,p,c)->(i,p,iota (k+(List.length i)) c)) br'
-	in MLcase(typ,e,new_br)
+        let new_br =
+          Array.map (fun (i,p,c)->(i,p,iota (k+(List.length i)) c)) br'
+        in MLcase(typ,e,new_br)
     | _ -> raise Impossible
   in iota 0 hd
 
@@ -1061,17 +1061,17 @@ let rec simpl o = function
   | MLletin(id,c,e) ->
       let e = simpl o e in
       if
-	(is_atomic c) || (is_atomic e) ||
-	(let n = nb_occur_match e in
-	 (Int.equal n 0 || (Int.equal n 1 && expand_linear_let o id e)))
+        (is_atomic c) || (is_atomic e) ||
+        (let n = nb_occur_match e in
+         (Int.equal n 0 || (Int.equal n 1 && expand_linear_let o id e)))
       then
-	simpl o (ast_subst c e)
+        simpl o (ast_subst c e)
       else
-	MLletin(id, simpl o c, e)
+        MLletin(id, simpl o c, e)
   | MLfix(i,ids,c) ->
       let n = Array.length ids in
       if ast_occurs_itvl 1 n c.(i) then
-	MLfix (i, ids, Array.map (simpl o) c)
+        MLfix (i, ids, Array.map (simpl o) c)
       else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
   | MLmagic(MLmagic _ as e) -> simpl o e
   | MLmagic(MLapp (f,l)) -> simpl o (MLapp (MLmagic f, l))
@@ -1094,12 +1094,12 @@ and simpl_app o a = function
       simpl o (MLapp (ast_pop t, List.tl a))
   | MLlam (id,t) -> (* Beta redex *)
       (match nb_occur_match t with
-	 | 0 -> simpl o (MLapp (ast_pop t, List.tl a))
-	 | 1 when (is_tmp id || o.opt_lin_beta) ->
-	     simpl o (MLapp (ast_subst (List.hd a) t, List.tl a))
-	 | _ ->
-	     let a' = List.map (ast_lift 1) (List.tl a) in
-	     simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
+         | 0 -> simpl o (MLapp (ast_pop t, List.tl a))
+         | 1 when (is_tmp id || o.opt_lin_beta) ->
+             simpl o (MLapp (ast_subst (List.hd a) t, List.tl a))
+         | _ ->
+             let a' = List.map (ast_lift 1) (List.tl a) in
+             simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
   | MLmagic (MLlam (id,t)) ->
       (* When we've at least one argument, we permute the magic
          and the lambda, to simplify things a bit (see #2795).
@@ -1111,14 +1111,14 @@ and simpl_app o a = function
   | MLcase (typ,e,br) when o.opt_case_app ->
       (* Application of a case: we push arguments inside *)
       let br' =
-	Array.map
-	  (fun (l,p,t) ->
-	     let k = List.length l in
-	     let a' = List.map (ast_lift k) a in
-	     (l, p, simpl o (MLapp (t,a')))) br
+        Array.map
+          (fun (l,p,t) ->
+             let k = List.length l in
+             let a' = List.map (ast_lift k) a in
+             (l, p, simpl o (MLapp (t,a')))) br
       in simpl o (MLcase (typ,e,br'))
   | (MLdummy _ | MLexn _) as e -> e
-	(* We just discard arguments in those cases. *)
+        (* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
 (* Invariant : all empty matches should now be [MLexn] *)
@@ -1139,19 +1139,19 @@ and simpl_case o typ br e =
       if lang() == Scheme || is_custom_match br
       then MLcase (typ, e, br)
       else match factor_branches o typ br with
-	| Some (f,ints) when Int.equal (Int.Set.cardinal ints) (Array.length br) ->
-	  (* If all branches have been factorized, we remove the match *)
-	  simpl o (MLletin (Tmp anonymous_name, e, f))
-	| Some (f,ints) ->
-	  let last_br =
-	    if ast_occurs 1 f then ([Tmp anonymous_name], Prel 1, f)
-	    else ([], Pwild, ast_pop f)
-	  in
-	  let brl = Array.to_list br in
-	  let brl_opt = List.filteri (fun i _ -> not (Int.Set.mem i ints)) brl in
-	  let brl_opt = brl_opt @ [last_br] in
-	  MLcase (typ, e, Array.of_list brl_opt)
-	| None -> MLcase (typ, e, br)
+        | Some (f,ints) when Int.equal (Int.Set.cardinal ints) (Array.length br) ->
+          (* If all branches have been factorized, we remove the match *)
+          simpl o (MLletin (Tmp anonymous_name, e, f))
+        | Some (f,ints) ->
+          let last_br =
+            if ast_occurs 1 f then ([Tmp anonymous_name], Prel 1, f)
+            else ([], Pwild, ast_pop f)
+          in
+          let brl = Array.to_list br in
+          let brl_opt = List.filteri (fun i _ -> not (Int.Set.mem i ints)) brl in
+          let brl_opt = brl_opt @ [last_br] in
+          MLcase (typ, e, Array.of_list brl_opt)
+        | None -> MLcase (typ, e, br)
 
 (*S Local prop elimination. *)
 (* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
@@ -1230,8 +1230,8 @@ let kill_dummy_lams sign c =
 let eta_expansion_sign s (ids,c) =
   let rec abs ids rels i = function
     | [] ->
-	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
-	in ids, MLapp (ast_lift (i-1) c, a)
+        let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
+        in ids, MLapp (ast_lift (i-1) c, a)
     | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l
     | Kill k :: l -> abs (Dummy :: ids) (MLdummy k :: rels) (i+1) l
   in abs ids [] 1 s
@@ -1275,14 +1275,14 @@ let kill_dummy_args (ids,bl) r t =
   in
   let rec killrec n = function
     | MLapp(e, a) when found n e ->
-	let k = max 0 (m - (List.length a)) in
-	let a = List.map (killrec n) a in
-	let a = List.map (ast_lift k) a in
-	let a = select_via_bl sign (a @ (eta_args k)) in
-	named_lams (List.firstn k ids) (MLapp (ast_lift k e, a))
+        let k = max 0 (m - (List.length a)) in
+        let a = List.map (killrec n) a in
+        let a = List.map (ast_lift k) a in
+        let a = select_via_bl sign (a @ (eta_args k)) in
+        named_lams (List.firstn k ids) (MLapp (ast_lift k e, a))
     | e when found n e ->
-	let a = select_via_bl sign (eta_args m) in
-	named_lams ids (MLapp (ast_lift m e, a))
+        let a = select_via_bl sign (eta_args m) in
+        named_lams ids (MLapp (ast_lift m e, a))
     | e -> ast_map_lift killrec n e
   in killrec 0 t
 
@@ -1294,32 +1294,32 @@ let sign_of_args a =
 let rec kill_dummy = function
   | MLfix(i,fi,c) ->
       (try
-	 let k,c = kill_dummy_fix i c [] in
-	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args k 1 (MLrel 1))
+         let k,c = kill_dummy_fix i c [] in
+         ast_subst (MLfix (i,fi,c)) (kill_dummy_args k 1 (MLrel 1))
        with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
   | MLapp (MLfix (i,fi,c),a) ->
       let a = List.map kill_dummy a in
       (* Heuristics: if some arguments are implicit args, we try to
          eliminate the corresponding arguments of the fixpoint *)
       (try
-	 let k,c = kill_dummy_fix i c (sign_of_args a) in
-	 let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in
-	 let fake' = kill_dummy_args k 1 fake in
-	 ast_subst (MLfix (i,fi,c)) fake'
+         let k,c = kill_dummy_fix i c (sign_of_args a) in
+         let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in
+         let fake' = kill_dummy_args k 1 fake in
+         ast_subst (MLfix (i,fi,c)) fake'
        with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a))
   | MLletin(id, MLfix (i,fi,c),e) ->
       (try
-	 let k,c = kill_dummy_fix i c [] in
-	 let e = kill_dummy (kill_dummy_args k 1 e) in
-	 MLletin(id, MLfix(i,fi,c),e)
+         let k,c = kill_dummy_fix i c [] in
+         let e = kill_dummy (kill_dummy_args k 1 e) in
+         MLletin(id, MLfix(i,fi,c),e)
       with Impossible ->
-	MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
+        MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
   | MLletin(id,c,e) ->
       (try
-	 let k,c = kill_dummy_lams [] (kill_dummy_hd c) in
-	 let e = kill_dummy (kill_dummy_args k 1 e) in
-	 let c = kill_dummy c in
-	 if is_atomic c then ast_subst c e else MLletin (id, c, e)
+         let k,c = kill_dummy_lams [] (kill_dummy_hd c) in
+         let e = kill_dummy (kill_dummy_args k 1 e) in
+         let c = kill_dummy c in
+         if is_atomic c then ast_subst c e else MLletin (id, c, e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
   | a -> ast_map kill_dummy a
 
@@ -1329,10 +1329,10 @@ and kill_dummy_hd = function
   | MLlam(id,e) -> MLlam(id, kill_dummy_hd e)
   | MLletin(id,c,e) ->
       (try
-	 let k,c = kill_dummy_lams [] (kill_dummy_hd c) in
-	 let e = kill_dummy_hd (kill_dummy_args k 1 e) in
-	 let c = kill_dummy c in
-	 if is_atomic c then ast_subst c e else MLletin (id, c, e)
+         let k,c = kill_dummy_lams [] (kill_dummy_hd c) in
+         let e = kill_dummy_hd (kill_dummy_args k 1 e) in
+         let c = kill_dummy c in
+         if is_atomic c then ast_subst c e else MLletin (id, c, e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e))
   | a -> a
 
@@ -1361,7 +1361,7 @@ let general_optimize_fix f ids n args m c =
   for i=0 to (n-1) do v.(i)<-i done;
   let aux i = function
     | MLrel j when v.(j-1)>=0 ->
-	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
+        if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
     | _ -> raise Impossible
   in List.iteri aux args;
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
@@ -1377,19 +1377,19 @@ let optimize_fix a =
     if Int.equal n 0 then a
     else match a' with
       | MLfix(_,[|f|],[|c|]) ->
-	  let new_f = MLapp (MLrel (n+1),eta_args n) in
-	  let new_c = named_lams ids (normalize (ast_subst new_f c))
-	  in MLfix(0,[|f|],[|new_c|])
+          let new_f = MLapp (MLrel (n+1),eta_args n) in
+          let new_c = named_lams ids (normalize (ast_subst new_f c))
+          in MLfix(0,[|f|],[|new_c|])
       | MLapp(a',args) ->
-	  let m = List.length args in
-	  (match a' with
-	     | MLfix(_,_,_) when
-		 (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a')
-		 -> a'
-	     | MLfix(_,[|f|],[|c|]) ->
-		 (try general_optimize_fix f ids n args m c
-		  with Impossible -> a)
-	     | _ -> a)
+          let m = List.length args in
+          (match a' with
+             | MLfix(_,_,_) when
+                 (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a')
+                 -> a'
+             | MLfix(_,[|f|],[|c|]) ->
+                 (try general_optimize_fix f ids n args m c
+                  with Impossible -> a)
+             | _ -> a)
       | _ -> a
 
 (*S Inlining. *)
@@ -1463,12 +1463,12 @@ let rec non_stricts add cand = function
       (* so we make an union (in fact a merge). *)
       let cand = non_stricts false cand t in
       Array.fold_left
-	(fun c (i,_,t)->
-	   let n = List.length i in
-	   let cand = lift n cand in
-	   let cand = pop n (non_stricts add cand t) in
-	   List.merge Int.compare cand c) [] v
-	(* [merge] may duplicates some indices, but I don't mind. *)
+        (fun c (i,_,t)->
+           let n = List.length i in
+           let cand = lift n cand in
+           let cand = pop n (non_stricts add cand t) in
+           List.merge Int.compare cand c) [] v
+        (* [merge] may duplicates some indices, but I don't mind. *)
   | MLmagic t ->
       non_stricts add cand t
   | _ ->
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index fe49bfc1ec..ec39beb03b 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -36,19 +36,19 @@ let se_iter do_decl do_spec do_mp =
     | MTident mp -> do_mp mp
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
     | MTwith (mt,ML_With_type(idl,l,t))->
-	let mp_mt = msid_of_mt mt in
-	let l',idl' = List.sep_last idl in
-	let mp_w =
-	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
-	in
+        let mp_mt = msid_of_mt mt in
+        let l',idl' = List.sep_last idl in
+        let mp_w =
+          List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
+        in
         let r = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l')) in
         mt_iter mt; do_spec (Stype(r,l,Some t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
         let mp_w =
-	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl
-	in
-	mt_iter mt; do_mp mp_w; do_mp mp
+          List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl
+        in
+        mt_iter mt; do_mp mp_w; do_mp mp
     | MTsig (_, sign) -> List.iter spec_iter sign
   and spec_iter = function
     | (_,Spec s) -> do_spec s
@@ -58,7 +58,7 @@ let se_iter do_decl do_spec do_mp =
   let rec se_iter = function
     | (_,SEdecl d) -> do_decl d
     | (_,SEmodule m) ->
-	me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
+        me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
     | (_,SEmodtype m) -> mt_iter m
   and me_iter = function
     | MEident mp -> do_mp mp
@@ -103,8 +103,8 @@ let ast_iter_references do_term do_cons do_type a =
       | MLglob r -> do_term r
       | MLcons (_,r,_) -> do_cons r
       | MLcase (ty,_,v) ->
-	type_iter_references do_type ty;
-	Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
+        type_iter_references do_type ty;
+        Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
 
       | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
       | MLdummy _ | MLaxiom | MLmagic _ | MLuint _ | MLfloat _ -> ()
@@ -118,7 +118,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
     if lang () == Ocaml then
       (match ind.ind_equiv with
          | Miniml.Equiv kne -> do_type (GlobRef.IndRef (MutInd.make1 kne, snd ip));
-	 | _ -> ());
+         | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
   if lang () == Ocaml then record_iter_references do_term ind.ind_kind;
@@ -132,7 +132,7 @@ let decl_iter_references do_term do_cons do_type =
     | Dtype (r,_,t) -> do_type r; type_iter t
     | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
     | Dfix(rv,c,t) ->
-	Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t
+        Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t
 
 let spec_iter_references do_term do_cons do_type = function
   | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
@@ -163,7 +163,7 @@ let rec type_search f = function
 let decl_type_search f = function
   | Dind (_,{ind_packets=p})  ->
       Array.iter
-	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
+        (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
   | Dterm (_,_,u) -> type_search f u
   | Dfix (_,_,v) -> Array.iter (type_search f) v
   | Dtype (_,_,u) -> type_search f u
@@ -171,7 +171,7 @@ let decl_type_search f = function
 let spec_type_search f = function
   | Sind (_,{ind_packets=p}) ->
       Array.iter
-	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
+        (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
   | Stype (_,_,ot) -> Option.iter (type_search f) ot
   | Sval (_,u) -> type_search f u
 
@@ -195,7 +195,7 @@ let rec msig_of_ms = function
   | (l,SEdecl (Dfix (rv,_,tv))) :: ms ->
       let msig = ref (msig_of_ms ms) in
       for i = Array.length rv - 1 downto 0 do
-	msig := (l,Spec (Sval (rv.(i),tv.(i))))::!msig
+        msig := (l,Spec (Sval (rv.(i),tv.(i))))::!msig
       done;
       !msig
   | (l,SEmodule m) :: ms -> (l,Smodule m.ml_mod_type) :: (msig_of_ms ms)
@@ -229,13 +229,13 @@ let get_decl_in_structure r struc =
     let rec go ll sel = match ll with
       | [] -> assert false
       | l :: ll ->
-	  match search_structure l (not (List.is_empty ll)) sel with
-	    | SEdecl d -> d
-	    | SEmodtype m -> assert false
-	    | SEmodule m ->
-		match m.ml_mod_expr with
-		  | MEstruct (_,sel) -> go ll sel
-		  | _ -> error_not_visible r
+          match search_structure l (not (List.is_empty ll)) sel with
+            | SEdecl d -> d
+            | SEmodtype m -> assert false
+            | SEmodule m ->
+                match m.ml_mod_expr with
+                  | MEstruct (_,sel) -> go ll sel
+                  | _ -> error_not_visible r
     in go ll sel
   with Not_found ->
     anomaly (Pp.str "reference not found in extracted structure.")
@@ -258,7 +258,7 @@ let dfix_to_mlfix rv av i =
   in
   let rec subst n t = match t with
     | MLglob ((GlobRef.ConstRef kn) as refe) ->
-	(try MLrel (n + (Refmap'.find refe s)) with Not_found -> t)
+        (try MLrel (n + (Refmap'.find refe s)) with Not_found -> t)
     | _ -> ast_map_lift subst n t
   in
   let ids = Array.map (fun r -> Label.to_id (label_of_r r)) rv in
@@ -277,9 +277,9 @@ let rec optim_se top to_appear s = function
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
       let d = match dump_unused_vars (optimize_fix a) with
-	| MLfix (0, _, [|c|]) ->
-	  Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
-	| a -> Dterm (r, a, t)
+        | MLfix (0, _, [|c|]) ->
+          Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
+        | a -> Dterm (r, a, t)
       in
       (l,SEdecl d) :: (optim_se top to_appear s lse)
   | (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
@@ -287,8 +287,8 @@ let rec optim_se top to_appear s = function
       (* This fake body ensures that no fixpoint will be auto-inlined. *)
       let fake_body = MLfix (0,[||],[||]) in
       for i = 0 to Array.length rv - 1 do
-	if inline rv.(i) fake_body
-	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
+        if inline rv.(i) fake_body
+        then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
       done;
       let av' = Array.map dump_unused_vars av in
       (l,SEdecl (Dfix (rv, av', tv))) :: (optim_se top to_appear s lse)
@@ -343,7 +343,7 @@ let compute_deps_decl = function
   | Dterm (r,u,t) ->
       type_iter_references add_needed t;
       if not (is_custom r) then
-	ast_iter_references add_needed add_needed add_needed u
+        ast_iter_references add_needed add_needed add_needed u
   | Dfix _ as d ->
       decl_iter_references add_needed add_needed add_needed d
 
@@ -370,10 +370,10 @@ let rec depcheck_se = function
       List.iter found_needed refs';
       (* Hack to avoid extracting unused part of a Dfix *)
       match d with
-	| Dfix (rv,trms,tys) when (List.for_all is_custom refs') ->
-	  let trms' =  Array.make (Array.length rv) (MLexn "UNUSED") in
-	  ((l,SEdecl (Dfix (rv,trms',tys))) :: se')
-	| _ -> (compute_deps_decl d; t::se')
+        | Dfix (rv,trms,tys) when (List.for_all is_custom refs') ->
+          let trms' =  Array.make (Array.length rv) (MLexn "UNUSED") in
+          ((l,SEdecl (Dfix (rv,trms',tys))) :: se')
+        | _ -> (compute_deps_decl d; t::se')
     end
   | t :: se ->
     let se' = depcheck_se se in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 34ddf57b40..66429833b9 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -163,16 +163,16 @@ let pp_type par vl t =
     | Tvar i -> (try pp_tvar (List.nth vl (pred i))
                  with Failure _ -> (str "'a" ++ int i))
     | Tglob (r,[a1;a2]) when is_infix r ->
-	pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
+        pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (GlobRef.IndRef(kn,0),l)
-	when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
-	pp_tuple_light pp_rec l
+        when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
+        pp_tuple_light pp_rec l
     | Tglob (r,l) ->
-	pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
+        pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
     | Tarr (t1,t2) ->
-	pp_par par
-	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
+        pp_par par
+          (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy _ -> str "__"
     | Tunknown -> str "__"
   in
@@ -209,101 +209,101 @@ let rec pp_expr par env args =
   and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
-	let id = get_db_name n env in
+        let id = get_db_name n env in
         (* Try to survive to the occurrence of a Dummy rel.
            TODO: we should get rid of this hack (cf. #592) *)
         let id = if Id.equal id dummy_name then Id.of_string "__" else id in
         apply (Id.print id)
     | MLapp (f,args') ->
-	let stl = List.map (pp_expr true env []) args' in
+        let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
     | MLlam _ as a ->
-      	let fl,a' = collect_lams a in
-	let fl = List.map id_of_mlid fl in
-	let fl,env' = push_vars fl env in
-	let st = pp_abst (List.rev fl) ++ pp_expr false env' [] a' in
-	apply2 st
+        let fl,a' = collect_lams a in
+        let fl = List.map id_of_mlid fl in
+        let fl,env' = push_vars fl env in
+        let st = pp_abst (List.rev fl) ++ pp_expr false env' [] a' in
+        apply2 st
     | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id_of_mlid id] env in
-	let pp_id = Id.print (List.hd i)
-	and pp_a1 = pp_expr false env [] a1
-	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
-	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
+        let i,env' = push_vars [id_of_mlid id] env in
+        let pp_id = Id.print (List.hd i)
+        and pp_a1 = pp_expr false env [] a1
+        and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
+        hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
     | MLglob r -> apply (pp_global Term r)
     | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
+        let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+        pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s ->
-	(* An [MLexn] may be applied, but I don't really care. *)
-	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
+        (* An [MLexn] may be applied, but I don't really care. *)
+        pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
     | MLdummy k ->
         (* An [MLdummy] may be applied, but I don't really care. *)
         (match msg_of_implicit k with
          | "" -> str "__"
          | s -> str "__" ++ spc () ++ str ("(* "^s^" *)"))
     | MLmagic a ->
-	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
+        pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
     | MLaxiom ->
-	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
+        pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
     | MLcons (_,r,a) as c ->
         assert (List.is_empty args);
         begin match a with
-	  | _ when is_native_char c -> pp_native_char c
-	  | [a1;a2] when is_infix r ->
-	    let pp = pp_expr true env [] in
-	    pp_par par (pp a1 ++ str (get_infix r) ++ pp a2)
-	  | _ when is_coinductive r ->
-	    let ne = not (List.is_empty a) in
-	    let tuple = space_if ne ++ pp_tuple (pp_expr true env []) a in
-	    pp_par par (str "lazy " ++ pp_par ne (pp_global Cons r ++ tuple))
-	  | [] -> pp_global Cons r
-	  | _ ->
-	    let fds = get_record_fields r in
-	    if not (List.is_empty fds) then
-	      pp_record_pat (pp_fields r fds, List.map (pp_expr true env []) a)
-	    else
-	      let tuple = pp_tuple (pp_expr true env []) a in
-	      if String.is_empty (str_global Cons r) (* hack Extract Inductive prod *)
-	      then tuple
-	      else pp_par par (pp_global Cons r ++ spc () ++ tuple)
-	end
+          | _ when is_native_char c -> pp_native_char c
+          | [a1;a2] when is_infix r ->
+            let pp = pp_expr true env [] in
+            pp_par par (pp a1 ++ str (get_infix r) ++ pp a2)
+          | _ when is_coinductive r ->
+            let ne = not (List.is_empty a) in
+            let tuple = space_if ne ++ pp_tuple (pp_expr true env []) a in
+            pp_par par (str "lazy " ++ pp_par ne (pp_global Cons r ++ tuple))
+          | [] -> pp_global Cons r
+          | _ ->
+            let fds = get_record_fields r in
+            if not (List.is_empty fds) then
+              pp_record_pat (pp_fields r fds, List.map (pp_expr true env []) a)
+            else
+              let tuple = pp_tuple (pp_expr true env []) a in
+              if String.is_empty (str_global Cons r) (* hack Extract Inductive prod *)
+              then tuple
+              else pp_par par (pp_global Cons r ++ spc () ++ tuple)
+        end
     | MLtuple l ->
         assert (List.is_empty args);
         pp_boxed_tuple (pp_expr true env []) l
     | MLcase (_, t, pv) when is_custom_match pv ->
         if not (is_regular_match pv) then
-	  user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
-	let mkfun (ids,_,e) =
-	  if not (List.is_empty ids) then named_lams (List.rev ids) e
-	  else dummy_lams (ast_lift 1 e) 1
-	in
-	let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
-	let inner =
-	  str (find_custom_match pv) ++ fnl () ++
-	  prvect pp_branch pv ++
-	  pp_expr true env [] t
-	in
-	apply2 (hov 2 inner)
+          user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
+        let mkfun (ids,_,e) =
+          if not (List.is_empty ids) then named_lams (List.rev ids) e
+          else dummy_lams (ast_lift 1 e) 1
+        in
+        let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
+        let inner =
+          str (find_custom_match pv) ++ fnl () ++
+          prvect pp_branch pv ++
+          pp_expr true env [] t
+        in
+        apply2 (hov 2 inner)
     | MLcase (typ, t, pv) ->
         let head =
-	  if not (is_coinductive_type typ) then pp_expr false env [] t
-	  else (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
-	in
-	(* First, can this match be printed as a mere record projection ? *)
+          if not (is_coinductive_type typ) then pp_expr false env [] t
+          else (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
+        in
+        (* First, can this match be printed as a mere record projection ? *)
         (try pp_record_proj par env typ t pv args
-	 with Impossible ->
-	   (* Second, can this match be printed as a let-in ? *)
-	   if Int.equal (Array.length pv) 1 then
-	     let s1,s2 = pp_one_pat env pv.(0) in
-	     hv 0 (apply2 (pp_letin s1 head s2))
-	   else
-	     (* Third, can this match be printed as [if ... then ... else] ? *)
-	     (try apply2 (pp_ifthenelse env head pv)
-	      with Not_found ->
-		(* Otherwise, standard match *)
-		apply2
-		  (v 0 (str "match " ++ head ++ str " with" ++ fnl () ++
-			pp_pat env pv))))
+         with Impossible ->
+           (* Second, can this match be printed as a let-in ? *)
+           if Int.equal (Array.length pv) 1 then
+             let s1,s2 = pp_one_pat env pv.(0) in
+             hv 0 (apply2 (pp_letin s1 head s2))
+           else
+             (* Third, can this match be printed as [if ... then ... else] ? *)
+             (try apply2 (pp_ifthenelse env head pv)
+              with Not_found ->
+                (* Otherwise, standard match *)
+                apply2
+                  (v 0 (str "match " ++ head ++ str " with" ++ fnl () ++
+                        pp_pat env pv))))
     | MLuint i ->
         assert (args=[]);
         str "(" ++ str (Uint63.compile i) ++ str ")"
@@ -381,9 +381,9 @@ and pp_ifthenelse env expr pv = match pv with
       ->
       hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
             hov 2 (str "then " ++
-		   hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++
-	    hov 2 (str "else " ++
-	           hov 2 (pp_expr (expr_needs_par els) env [] els)))
+                   hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++
+            hov 2 (str "else " ++
+                   hov 2 (pp_expr (expr_needs_par els) env [] els)))
   | _ -> raise Not_found
 
 and pp_one_pat env (ids,p,t) =
@@ -404,20 +404,20 @@ and pp_function env t =
   let bl,env' = push_vars (List.map id_of_mlid bl) env in
   match t' with
     | MLcase(Tglob(r,_),MLrel 1,pv) when
-	not (is_coinductive r) && List.is_empty (get_record_fields r) &&
-	not (is_custom_match pv) ->
-	if not (ast_occurs 1 (MLcase(Tunknown,MLaxiom,pv))) then
-	  pr_binding (List.rev (List.tl bl)) ++
-       	  str " = function" ++ fnl () ++
-	  v 0 (pp_pat env' pv)
-	else
+        not (is_coinductive r) && List.is_empty (get_record_fields r) &&
+        not (is_custom_match pv) ->
+        if not (ast_occurs 1 (MLcase(Tunknown,MLaxiom,pv))) then
+          pr_binding (List.rev (List.tl bl)) ++
+          str " = function" ++ fnl () ++
+          v 0 (pp_pat env' pv)
+        else
           pr_binding (List.rev bl) ++
           str " = match " ++ Id.print (List.hd bl) ++ str " with" ++ fnl () ++
-	  v 0 (pp_pat env' pv)
+          v 0 (pp_pat env' pv)
     | _ ->
           pr_binding (List.rev bl) ++
-	  str " =" ++ fnl () ++ str "  " ++
-	  hov 2 (pp_expr false env' [] t')
+          str " =" ++ fnl () ++ str "  " ++
+          hov 2 (pp_expr false env' [] t')
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
@@ -425,12 +425,12 @@ and pp_function env t =
 and pp_fix par env i (ids,bl) args =
   pp_par par
     (v 0 (str "let rec " ++
-	  prvect_with_sep
-      	    (fun () -> fnl () ++ str "and ")
-	    (fun (fi,ti) -> Id.print fi ++ pp_function env ti)
-	    (Array.map2 (fun id b -> (id,b)) ids bl) ++
-	  fnl () ++
-	  hov 2 (str "in " ++ pp_apply (Id.print ids.(i)) false args)))
+          prvect_with_sep
+            (fun () -> fnl () ++ str "and ")
+            (fun (fi,ti) -> Id.print fi ++ pp_function env ti)
+            (Array.map2 (fun id b -> (id,b)) ids bl) ++
+          fnl () ++
+          hov 2 (str "in " ++ pp_apply (Id.print ids.(i)) false args)))
 
 (* Ad-hoc double-newline in v boxes, with enough negative whitespace
    to avoid indenting the intermediate blank line *)
@@ -451,19 +451,19 @@ let pp_Dfix (rv,c,t) =
     if i >= Array.length rv then mt ()
     else
       let void = is_inline_custom rv.(i) ||
-	(not (is_custom rv.(i)) &&
+        (not (is_custom rv.(i)) &&
          match c.(i) with MLexn "UNUSED" -> true | _ -> false)
       in
       if void then pp init (i+1)
       else
-	let def =
-	  if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
-	  else pp_function (empty_env ()) c.(i)
-	in
-	(if init then mt () else cut2 ()) ++
-	pp_val names.(i) t.(i) ++
-	str (if init then "let rec " else "and ") ++ names.(i) ++ def ++
-	pp false (i+1)
+        let def =
+          if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
+          else pp_function (empty_env ()) c.(i)
+        in
+        (if init then mt () else cut2 ()) ++
+        pp_val names.(i) t.(i) ++
+        str (if init then "let rec " else "and ") ++ names.(i) ++ def ++
+        pp false (i+1)
   in pp true 0
 
 (*s Pretty-printing of inductive types declaration. *)
@@ -481,9 +481,9 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   let pp_constructor i typs =
     (if Int.equal i 0 then mt () else fnl ()) ++
     hov 3 (str "| " ++ cnames.(i) ++
-	   (if List.is_empty typs then mt () else str " of ") ++
-	   prlist_with_sep
-	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
+           (if List.is_empty typs then mt () else str " of ") ++
+           prlist_with_sep
+            (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
   in
   pp_parameters pl ++ str prefix ++ name ++
   pp_equiv pl name ip_equiv ++ str " =" ++
@@ -494,16 +494,16 @@ let pp_logical_ind packet =
   pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
   fnl () ++
   pp_comment (str "with constructors : " ++
-	      prvect_with_sep spc Id.print packet.ip_consnames) ++
+              prvect_with_sep spc Id.print packet.ip_consnames) ++
   fnl ()
 
 let pp_singleton kn packet =
   let name = pp_global Type (GlobRef.IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
-	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment (str "singleton inductive, whose constructor was " ++
-		     Id.print packet.ip_consnames.(0)))
+         pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
+         pp_comment (str "singleton inductive, whose constructor was " ++
+                     Id.print packet.ip_consnames.(0)))
 
 let pp_record kn fields ip_equiv packet =
   let ind = GlobRef.IndRef (kn,0) in
@@ -514,7 +514,7 @@ let pp_record kn fields ip_equiv packet =
   str "type " ++ pp_parameters pl ++ name ++
   pp_equiv pl name ip_equiv ++ str " = { "++
   hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ())
-	   (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l)
+           (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l)
   ++ str " }"
 
 let pp_coind pl name =
@@ -536,7 +536,7 @@ let pp_ind co kn ind =
     Array.mapi
       (fun i p -> if p.ip_logical then [||] else
          Array.mapi (fun j _ -> pp_global Cons (GlobRef.ConstructRef ((kn,i),j+1)))
-	   p.ip_types)
+           p.ip_types)
       ind.ind_packets
   in
   let rec pp i kwd =
@@ -548,9 +548,9 @@ let pp_ind co kn ind =
       if is_custom (GlobRef.IndRef ip) then pp (i+1) kwd
       else if p.ip_logical then pp_logical_ind p ++ pp (i+1) kwd
       else
-	kwd ++ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
-	pp_one_ind prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
-	pp (i+1) nextkwd
+        kwd ++ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
+        pp_one_ind prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
+        pp (i+1) nextkwd
   in
   pp 0 initkwd
 
@@ -570,26 +570,26 @@ let pp_decl = function
     | Dind (kn,i) -> pp_mind kn i
     | Dtype (r, l, t) ->
         let name = pp_global Type r in
-	let l = rename_tvars keywords l in
+        let l = rename_tvars keywords l in
         let ids, def =
-	  try
-	    let ids,s = find_type_custom r in
-	    pp_string_parameters ids, str " =" ++ spc () ++ str s
-	  with Not_found ->
-	    pp_parameters l,
-	    if t == Taxiom then str " (* AXIOM TO BE REALIZED *)"
-	    else str " =" ++ spc () ++ pp_type false l t
-	in
-	hov 2 (str "type " ++ ids ++ name ++ def)
+          try
+            let ids,s = find_type_custom r in
+            pp_string_parameters ids, str " =" ++ spc () ++ str s
+          with Not_found ->
+            pp_parameters l,
+            if t == Taxiom then str " (* AXIOM TO BE REALIZED *)"
+            else str " =" ++ spc () ++ pp_type false l t
+        in
+        hov 2 (str "type " ++ ids ++ name ++ def)
     | Dterm (r, a, t) ->
-	let def =
-	  if is_custom r then str (" = " ^ find_custom r)
-	  else pp_function (empty_env ()) a
-	in
-	let name = pp_global Term r in
+        let def =
+          if is_custom r then str (" = " ^ find_custom r)
+          else pp_function (empty_env ()) a
+        in
+        let name = pp_global Term r in
         pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ mt ())
     | Dfix (rv,defs,typs) ->
-	pp_Dfix (rv,defs,typs)
+        pp_Dfix (rv,defs,typs)
 
 let pp_spec = function
   | Sval (r,_) when is_inline_custom r -> mt ()
@@ -603,15 +603,15 @@ let pp_spec = function
       let name = pp_global Type r in
       let l = rename_tvars keywords vl in
       let ids, def =
-	try
-	  let ids, s = find_type_custom r in
-	  pp_string_parameters ids, str " =" ++ spc () ++ str s
-	with Not_found ->
-	  let ids = pp_parameters l in
-	  match ot with
-	    | None -> ids, mt ()
-	    | Some Taxiom -> ids, str " (* AXIOM TO BE REALIZED *)"
-	    | Some t -> ids, str " =" ++ spc () ++ pp_type false l t
+        try
+          let ids, s = find_type_custom r in
+          pp_string_parameters ids, str " =" ++ spc () ++ str s
+        with Not_found ->
+          let ids = pp_parameters l in
+          match ot with
+            | None -> ids, mt ()
+            | Some Taxiom -> ids, str " (* AXIOM TO BE REALIZED *)"
+            | Some t -> ids, str " =" ++ spc () ++ pp_type false l t
       in
       hov 2 (str "type " ++ ids ++ name ++ def)
 
@@ -621,8 +621,8 @@ let rec pp_specif = function
      (match Common.get_duplicate (top_visible_mp ()) l with
       | None -> pp_spec s
       | Some ren ->
-	 hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
-	 fnl () ++ str "end" ++ fnl () ++
+         hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
+         fnl () ++ str "end" ++ fnl () ++
          str ("include module type of struct include "^ren^" end"))
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
@@ -670,7 +670,7 @@ and pp_module_type params = function
       let mp_mt = msid_of_mt mt in
       let l,idl' = List.sep_last idl in
       let mp_w =
-	List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
+        List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
       in
       let r = GlobRef.ConstRef (Constant.make2 mp_w (Label.of_id l)) in
       push_visible mp_mt [];
@@ -680,7 +680,7 @@ and pp_module_type params = function
   | MTwith(mt,ML_With_module(idl,mp)) ->
       let mp_mt = msid_of_mt mt in
       let mp_w =
-	List.fold_left (fun mp id -> MPdot(mp,Label.of_id id)) mp_mt idl
+        List.fold_left (fun mp id -> MPdot(mp,Label.of_id id)) mp_mt idl
       in
       push_visible mp_mt [];
       let pp_w = str " with module " ++ pp_modname mp_w in
@@ -694,20 +694,20 @@ let rec pp_structure_elem = function
      (match Common.get_duplicate (top_visible_mp ()) l with
       | None -> pp_decl d
       | Some ren ->
-	 hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
-	 fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
+         hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
+         fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
-	if Common.get_phase () == Pre then
-	  str ": " ++ pp_module_type [] m.ml_mod_type
-	else mt ()
+        if Common.get_phase () == Pre then
+          str ": " ++ pp_module_type [] m.ml_mod_type
+        else mt ()
       in
       let def = pp_module_expr [] m.ml_mod_expr in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1
-	(str "module " ++ name ++ typ ++ str " =" ++
-	 (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
+        (str "module " ++ name ++ typ ++ str " =" ++
+         (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
       (match Common.get_duplicate (top_visible_mp ()) l with
        | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
        | None -> mt ())
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index c341ec8d57..c41b0d7a02 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -50,13 +50,13 @@ let pp_abst st = function
   | [] -> assert false
   | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
   | l -> paren
-	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
+        (str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
 
 let pp_apply st _ = function
   | [] -> st
   | [a] -> hov 2 (paren (st ++ spc () ++ a))
   | args -> hov 2 (paren (str "@ " ++ st ++
-			  (prlist_strict (fun x -> spc () ++ x) args)))
+                          (prlist_strict (fun x -> spc () ++ x) args)))
 
 (*s The pretty-printer for Scheme syntax *)
 
@@ -68,66 +68,66 @@ let rec pp_expr env args =
   let apply st = pp_apply st true args in
   function
     | MLrel n ->
-	let id = get_db_name n env in apply (pr_id id)
+        let id = get_db_name n env in apply (pr_id id)
     | MLapp (f,args') ->
-	let stl = List.map (pp_expr env []) args' in
+        let stl = List.map (pp_expr env []) args' in
         pp_expr env (stl @ args) f
     | MLlam _ as a ->
-      	let fl,a' = collect_lams a in
-	let fl,env' = push_vars (List.map id_of_mlid fl) env in
-	apply (pp_abst (pp_expr env' [] a') (List.rev fl))
+        let fl,a' = collect_lams a in
+        let fl,env' = push_vars (List.map id_of_mlid fl) env in
+        apply (pp_abst (pp_expr env' [] a') (List.rev fl))
     | MLletin (id,a1,a2) ->
-	let i,env' = push_vars [id_of_mlid id] env in
-	apply
-	  (hv 0
-	     (hov 2
-		(paren
-		   (str "let " ++
-		    paren
-		      (paren
-			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1))
-		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
+        let i,env' = push_vars [id_of_mlid id] env in
+        apply
+          (hv 0
+             (hov 2
+                (paren
+                   (str "let " ++
+                    paren
+                      (paren
+                         (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1))
+                    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r ->
-	apply (pp_global Term r)
+        apply (pp_global Term r)
     | MLcons (_,r,args') ->
-	assert (List.is_empty args);
-	let st =
-	  str "`" ++
-	  paren (pp_global Cons r ++
-		 (if List.is_empty args' then mt () else spc ()) ++
-		 prlist_with_sep spc (pp_cons_args env) args')
-	in
-	if is_coinductive r then paren (str "delay " ++ st) else st
+        assert (List.is_empty args);
+        let st =
+          str "`" ++
+          paren (pp_global Cons r ++
+                 (if List.is_empty args' then mt () else spc ()) ++
+                 prlist_with_sep spc (pp_cons_args env) args')
+        in
+        if is_coinductive r then paren (str "delay " ++ st) else st
     | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Scheme yet.")
     | MLcase (_,_,pv) when not (is_regular_match pv) ->
-	user_err Pp.(str "Cannot handle general patterns in Scheme yet.")
+        user_err Pp.(str "Cannot handle general patterns in Scheme yet.")
     | MLcase (_,t,pv) when is_custom_match pv ->
-	let mkfun (ids,_,e) =
-	  if not (List.is_empty ids) then named_lams (List.rev ids) e
-	  else dummy_lams (ast_lift 1 e) 1
-	in
-	apply
-	  (paren
-	     (hov 2
-		(str (find_custom_match pv) ++ fnl () ++
-		 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
-		 ++ pp_expr env [] t)))
+        let mkfun (ids,_,e) =
+          if not (List.is_empty ids) then named_lams (List.rev ids) e
+          else dummy_lams (ast_lift 1 e) 1
+        in
+        apply
+          (paren
+             (hov 2
+                (str (find_custom_match pv) ++ fnl () ++
+                 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
+                 ++ pp_expr env [] t)))
     | MLcase (typ,t, pv) ->
         let e =
-	  if not (is_coinductive_type typ) then pp_expr env [] t
-	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
-	in
-	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
+          if not (is_coinductive_type typ) then pp_expr env [] t
+          else paren (str "force" ++ spc () ++ pp_expr env [] t)
+        in
+        apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
     | MLfix (i,ids,defs) ->
-	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix env' i (Array.of_list (List.rev ids'),defs) args
+        let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+        pp_fix env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s ->
-	(* An [MLexn] may be applied, but I don't really care. *)
-	paren (str "error" ++ spc () ++ qs s)
+        (* An [MLexn] may be applied, but I don't really care. *)
+        paren (str "error" ++ spc () ++ qs s)
     | MLdummy _ ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
+        str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLmagic a ->
-	pp_expr env args a
+        pp_expr env args a
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
     | MLuint _ ->
       paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
@@ -137,8 +137,8 @@ let rec pp_expr env args =
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->
       paren (pp_global Cons r ++
-	     (if List.is_empty args then mt () else spc ()) ++
-	     prlist_with_sep spc (pp_cons_args env) args)
+             (if List.is_empty args then mt () else spc ()) ++
+             prlist_with_sep spc (pp_cons_args env) args)
   | e -> str "," ++ pp_expr env [] e
 
 and pp_one_pat env (ids,p,t) =
@@ -166,12 +166,12 @@ and pp_fix env j (ids,bl) args =
     paren
       (str "letrec " ++
        (v 0 (paren
-	       (prvect_with_sep fnl
-		  (fun (fi,ti) ->
-		     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
-		  (Array.map2 (fun id b -> (id,b)) ids bl)) ++
-	     fnl () ++
-      	     hov 2 (pp_apply (pr_id (ids.(j))) true args))))
+               (prvect_with_sep fnl
+                  (fun (fi,ti) ->
+                     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
+                  (Array.map2 (fun id b -> (id,b)) ids bl)) ++
+             fnl () ++
+             hov 2 (pp_apply (pr_id (ids.(j))) true args))))
 
 (*s Pretty-printing of a declaration. *)
 
@@ -180,29 +180,29 @@ let pp_decl = function
   | Dtype _ -> mt ()
   | Dfix (rv, defs,_) ->
       let names = Array.map
-	(fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+        (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
       in
       prvecti
-	(fun i r ->
-	  let void = is_inline_custom r ||
-	    (not (is_custom r) &&
+        (fun i r ->
+          let void = is_inline_custom r ||
+            (not (is_custom r) &&
              match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
-	  in
-	  if void then mt ()
-	  else
-	    hov 2
-	      (paren (str "define " ++ names.(i) ++ spc () ++
-			(if is_custom r then str (find_custom r)
-			 else pp_expr (empty_env ()) [] defs.(i)))
-	       ++ fnl ()) ++ fnl ())
-	rv
+          in
+          if void then mt ()
+          else
+            hov 2
+              (paren (str "define " ++ names.(i) ++ spc () ++
+                        (if is_custom r then str (find_custom r)
+                         else pp_expr (empty_env ()) [] defs.(i)))
+               ++ fnl ()) ++ fnl ())
+        rv
   | Dterm (r, a, _) ->
       if is_inline_custom r then mt ()
       else
-	hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
-			(if is_custom r then str (find_custom r)
-			 else pp_expr (empty_env ()) [] a)))
-	++ fnl2 ()
+        hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
+                        (if is_custom r then str (find_custom r)
+                         else pp_expr (empty_env ()) [] a)))
+        ++ fnl2 ()
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index be9259861a..7b64706138 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -289,7 +289,7 @@ let safe_pr_long_global r =
   with Not_found -> match r with
     | GlobRef.ConstRef kn ->
         let mp,l = Constant.repr2 kn in
-	str ((ModPath.to_string mp)^"."^(Label.to_string l))
+        str ((ModPath.to_string mp)^"."^(Label.to_string l))
     | _ -> assert false
 
 let pr_long_mp mp =
@@ -339,10 +339,10 @@ let warn_extraction_opaque_accessed =
 let warn_extraction_opaque_as_axiom =
   CWarnings.create ~name:"extraction-opaque-as-axiom" ~category:"extraction"
     (fun lst -> strbrk "The extraction now honors the opacity constraints by default, " ++
-	 strbrk "the following opaque constants have been extracted as axioms :" ++
-	 lst ++ str "." ++ fnl () ++
-	 strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this."
-	 ++ fnl ())
+         strbrk "the following opaque constants have been extracted as axioms :" ++
+         lst ++ str "." ++ fnl () ++
+         strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this."
+         ++ fnl ())
 
 let warning_opaques accessed =
   let opaques = Refset'.elements !opaques in
@@ -375,14 +375,14 @@ let warn_extraction_inside_module =
 let check_inside_module () =
   if Lib.is_modtype () then
     err (str "You can't do that within a Module Type." ++ fnl () ++
-	 str "Close it and try again.")
+         str "Close it and try again.")
   else if Lib.is_module () then
     warn_extraction_inside_module ()
 
 let check_inside_section () =
   if Global.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
-	 str "Close it and try again.")
+         str "Close it and try again.")
 
 let warn_extraction_reserved_identifier =
   CWarnings.create ~name:"extraction-reserved-identifier" ~category:"extraction"
@@ -441,9 +441,9 @@ let error_MPfile_as_mod mp b =
   let s1 = if b then "asked" else "required" in
   let s2 = if b then "extract some objects of this module or\n" else "" in
   err (str ("Extraction of file "^(raw_string_of_modfile mp)^
-	    ".v as a module is "^s1^".\n"^
-	    "Monolithic Extraction cannot deal with this situation.\n"^
-	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
+            ".v as a module is "^s1^".\n"^
+            "Monolithic Extraction cannot deal with this situation.\n"^
+            "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
 let argnames_of_global r =
   let env = Global.env () in
@@ -481,10 +481,10 @@ let warning_remaining_implicit k =
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
       if not (Library.library_is_loaded dp) then begin
-	match base_mp (Lib.current_mp ()) with
-	  | MPfile dp' when not (DirPath.equal dp dp') ->
+        match base_mp (Lib.current_mp ()) with
+          | MPfile dp' when not (DirPath.equal dp dp') ->
             err (str "Please load library " ++ DirPath.print dp ++ str " first.")
-	  | _ -> ()
+          | _ -> ()
       end
   | _ -> ()
 
@@ -574,11 +574,11 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
 let optims () = !opt_flag_ref
 
 let () = declare_bool_option
-	  {optdepr = false;
-	   optname = "Extraction Optimize";
-	   optkey = ["Extraction"; "Optimize"];
-	   optread = (fun () -> not (Int.equal !int_flag_ref 0));
-	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
+          {optdepr = false;
+           optname = "Extraction Optimize";
+           optkey = ["Extraction"; "Optimize"];
+           optread = (fun () -> not (Int.equal !int_flag_ref 0));
+           optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
 
 let () = declare_int_option
           { optdepr = false;
@@ -671,11 +671,11 @@ let print_extraction_inline () =
     (str "Extraction Inline:" ++ fnl () ++
      Refset'.fold
        (fun r p ->
-	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
+          (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++
      Refset'.fold
        (fun r p ->
-	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
+          (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
 
 (* Reset part *)
 
@@ -708,16 +708,16 @@ let add_implicits r l =
   let n = List.length names in
   let add_arg s = function
     | ArgInt i ->
-	if 1 <= i && i <= n then Int.Set.add i s
-	else err (int i ++ str " is not a valid argument number for " ++
-		  safe_pr_global r)
+        if 1 <= i && i <= n then Int.Set.add i s
+        else err (int i ++ str " is not a valid argument number for " ++
+                  safe_pr_global r)
     | ArgId id ->
        try
          let i = List.index Name.equal (Name id) names in
          Int.Set.add i s
        with Not_found ->
-	 err (str "No argument " ++ Id.print id ++ str " for " ++
-	      safe_pr_global r)
+         err (str "No argument " ++ Id.print id ++ str " for " ++
+              safe_pr_global r)
   in
   let ints = List.fold_left add_arg Int.Set.empty l in
   implicits_table := Refmap'.add r ints !implicits_table
@@ -854,16 +854,16 @@ let extract_constant_inline inline r ids s =
   let g = Smartlocate.global_with_alias r in
   match g with
     | GlobRef.ConstRef kn ->
-	let env = Global.env () in
+        let env = Global.env () in
         let typ, _ = Typeops.type_of_global_in_context env (GlobRef.ConstRef kn) in
-	let typ = Reduction.whd_all env typ in
-	if Reduction.is_arity env typ
-	  then begin
-	    let nargs = Hook.get use_type_scheme_nb_args env typ in
-	    if not (Int.equal (List.length ids) nargs) then error_axiom_scheme g nargs
-	  end;
-	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
-	Lib.add_anonymous_leaf (in_customs (g,ids,s))
+        let typ = Reduction.whd_all env typ in
+        if Reduction.is_arity env typ
+          then begin
+            let nargs = Hook.get use_type_scheme_nb_args env typ in
+            if not (Int.equal (List.length ids) nargs) then error_axiom_scheme g nargs
+          end;
+        Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
+        Lib.add_anonymous_leaf (in_customs (g,ids,s))
     | _ -> error_constant g
 
 
@@ -873,18 +873,18 @@ let extract_inductive r s l optstr =
   Dumpglob.add_glob ?loc:r.CAst.loc g;
   match g with
     | GlobRef.IndRef ((kn,i) as ip) ->
-	let mib = Global.lookup_mind kn in
-	let n = Array.length mib.mind_packets.(i).mind_consnames in
-	if not (Int.equal n (List.length l)) then error_nb_cons ();
-	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
-	Lib.add_anonymous_leaf (in_customs (g,[],s));
-	Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
-	  optstr;
-	List.iteri
-	  (fun j s ->
+        let mib = Global.lookup_mind kn in
+        let n = Array.length mib.mind_packets.(i).mind_consnames in
+        if not (Int.equal n (List.length l)) then error_nb_cons ();
+        Lib.add_anonymous_leaf (inline_extraction (true,[g]));
+        Lib.add_anonymous_leaf (in_customs (g,[],s));
+        Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
+          optstr;
+        List.iteri
+          (fun j s ->
              let g = GlobRef.ConstructRef (ip,succ j) in
-	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
-	     Lib.add_anonymous_leaf (in_customs (g,[],s))) l
+             Lib.add_anonymous_leaf (inline_extraction (true,[g]));
+             Lib.add_anonymous_leaf (in_customs (g,[],s))) l
     | _ -> error_inductive g