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

44 files changed, 1324 insertions, 1324 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 72585e5014..af08ea18c1 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -53,10 +53,10 @@ let reset () =
 
 let stop() =
   Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
-	 str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
-	 int !evar ++ str" match=" ++ int !nb_match ++ str" fix=" ++ int !fix ++
+         str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++
+         int !evar ++ str" match=" ++ int !nb_match ++ str" fix=" ++ int !fix ++
          str " cofix=" ++ int !cofix ++ str" prune=" ++ int !prune ++
-	 str"]")
+         str"]")
 
 let incr_cnt red cnt =
   if red then begin
@@ -119,7 +119,7 @@ module RedFlags : RedFlagsSig = struct
 
   type red_kind = BETA | DELTA | ETA | MATCH | FIX
               | COFIX | ZETA
-	      | CONST of Constant.t | VAR of Id.t
+              | CONST of Constant.t | VAR of Id.t
   let fBETA = BETA
   let fDELTA = DELTA
   let fETA = ETA
@@ -181,16 +181,16 @@ module RedFlags : RedFlagsSig = struct
     | ETA -> incr_cnt red.r_eta eta
     | CONST kn ->
       let c = is_transparent_constant red.r_const kn in
-	incr_cnt c delta
+        incr_cnt c delta
     | VAR id -> (* En attendant d'avoir des kn pour les Var *)
       let c = is_transparent_variable red.r_const id in
-	incr_cnt c delta
+        incr_cnt c delta
     | ZETA -> incr_cnt red.r_zeta zeta
     | MATCH -> incr_cnt red.r_match nb_match
     | FIX -> incr_cnt red.r_fix fix
     | COFIX -> incr_cnt red.r_cofix cofix
     | DELTA -> (* Used for Rel/Var defined in context *)
-	incr_cnt red.r_delta delta
+        incr_cnt red.r_delta delta
 
   let red_projection red p =
     if Projection.unfolded p then true
@@ -824,10 +824,10 @@ let rec try_drop_parameters depth n = function
           reloc_rargs depth (append_stack aft s)
     | Zshift(k)::s -> try_drop_parameters (depth-k) n s
     | [] ->
-	if Int.equal n 0 then []
-	else raise Not_found
+        if Int.equal n 0 then []
+        else raise Not_found
     | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zprimitive _) :: _ -> assert false
-	(* strip_update_shift_app only produces Zapp and Zshift items *)
+        (* strip_update_shift_app only produces Zapp and Zshift items *)
 
 let drop_parameters depth n argstk =
   try try_drop_parameters depth n argstk
@@ -852,7 +852,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
   match Declareops.inductive_make_projections ind mib with
   | Some projs ->
     (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
-	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
+           arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
     let pars = mib.Declarations.mind_nparams in
     let right = fapp_stack (f, s') in
     let (depth, args, _s) = strip_update_shift_app m s in
@@ -869,8 +869,8 @@ let eta_expand_ind_stack env ind m s (f, s') =
 let rec project_nth_arg n = function
   | Zapp args :: s ->
       let q = Array.length args in
-	if n >= q then project_nth_arg (n - q) s
-	else (* n < q *) args.(n)
+        if n >= q then project_nth_arg (n - q) s
+        else (* n < q *) args.(n)
   | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _ | Zprimitive _) :: _ | [] -> assert false
       (* After drop_parameters we have a purely applicative stack *)
 
@@ -891,12 +891,12 @@ let contract_fix_vect fix =
           (bds.(i),
            (fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance);
                        term = FFix (((reci,j),rdcl),env) }),
-	   env, Array.length bds)
+           env, Array.length bds)
       | FCoFix ((i,(nas,_,bds as rdcl)),env) ->
           (bds.(i),
            (fun j -> { mark = mark Cstr (opt_of_rel nas.(j).binder_relevance);
                        term = FCoFix ((j,rdcl),env) }),
-	   env, Array.length bds)
+           env, Array.length bds)
       | _ -> assert false
   in
   (subs_cons(Array.init nfix make_body, env), thisbody)
@@ -1347,11 +1347,11 @@ let rec zip_term zfun m stk =
         zip_term zfun (mkApp(m, Array.map zfun args)) s
     | ZcaseT(ci,p,br,e)::s ->
         let t = mkCase(ci, zfun (mk_clos e p), m,
-		       Array.map (fun b -> zfun (mk_clos e b)) br) in
+                       Array.map (fun b -> zfun (mk_clos e b)) br) in
         zip_term zfun t s
     | Zproj p::s ->
         let t = mkProj (Projection.make p true, m) in
-	zip_term zfun t s
+        zip_term zfun t s
     | Zfix(fx,par)::s ->
         let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in
         zip_term zfun h s
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 009db05ea2..e33a4f1518 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -106,18 +106,18 @@ let rec pp_instr i =
       str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
   | Kclosurerec(fv,init,lblt,lblb) ->
       h 1 (str "closurerec " ++
-	     int fv ++ str ", " ++ int init ++
-	     str " types = " ++
-	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
-	     str " bodies = " ++
-	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
+             int fv ++ str ", " ++ int init ++
+             str " types = " ++
+             prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+             str " bodies = " ++
+             prlist_with_sep spc pp_lbl (Array.to_list lblb))
   | Kclosurecofix (fv,init,lblt,lblb) ->
       h 1 (str "closurecofix " ++
-	     int fv ++ str ", " ++ int init ++
-	     str " types = " ++
-	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
-	     str " bodies = " ++
-	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
+             int fv ++ str ", " ++ int init ++
+             str " types = " ++
+             prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+             str " bodies = " ++
+             prlist_with_sep spc pp_lbl (Array.to_list lblb))
   | Kgetglobal idu -> str "getglobal " ++ Constant.print idu
   | Kconst sc ->
       str "const " ++ pp_struct_const sc
@@ -126,12 +126,12 @@ let rec pp_instr i =
   | Kmakeprod -> str "makeprod"
   | Kmakeswitchblock(lblt,lbls,_,sz) ->
       str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
-	pp_lbl lbls ++ str ", " ++ int sz
+        pp_lbl lbls ++ str ", " ++ int sz
   | Kswitch(lblc,lblb) ->
       h 1 (str "switch " ++
-	     prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
-	     str " | " ++
-	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
+             prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
+             str " | " ++
+             prlist_with_sep spc pp_lbl (Array.to_list lblb))
   | Kpushfields n -> str "pushfields " ++ int n
   | Kfield n -> str "field " ++ int n
   | Ksetfield n -> str "setfield " ++ int n
@@ -153,8 +153,8 @@ and pp_bytecodes c =
   match c with
   | [] -> str ""
   | Klabel lbl :: c ->
-	str "L" ++ int lbl ++ str ":" ++ fnl () ++
-	pp_bytecodes c
+        str "L" ++ int lbl ++ str ":" ++ fnl () ++
+        pp_bytecodes c
   | Ksequence (l1, l2) :: c ->
       pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
   | i :: c ->
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 06b380ef89..d7ea6f13c2 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -46,7 +46,7 @@ type instruction =
   | Kconst of structured_constant
   | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
                                          ** is accu, all others are popped from
-					 ** the top of the stack  *)
+                                         ** the top of the stack  *)
   | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
   | Kswitch of Label.t array * Label.t array (** consts,blocks *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 13cc6f7ea4..985c692eea 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -292,9 +292,9 @@ let pos_rel i r sz =
       let env = !(r.in_env) in
       try Kenvacc(r.offset + find_at db env)
       with Not_found ->
-	let pos = env.size in
-	r.in_env := push_fv db env;
-	Kenvacc(r.offset + pos)
+        let pos = env.size in
+        r.in_env := push_fv db env;
+        Kenvacc(r.offset + pos)
 
 let pos_universe_var i r sz =
   (* Compilation of a universe variable can happen either at toplevel (the
@@ -445,7 +445,7 @@ let nest_block tag arity cont =
   Kconst (Const_b0 (tag - Obj.last_non_constant_constructor_tag)) ::
     Kmakeblock(arity+1, Obj.last_non_constant_constructor_tag) :: cont
 
-let code_makeblock ~stack_size ~arity ~tag cont = 
+let code_makeblock ~stack_size ~arity ~tag cont =
   if tag < Obj.last_non_constant_constructor_tag then
     Kmakeblock(arity, tag) :: cont
   else begin
@@ -473,16 +473,16 @@ let comp_app comp_fun comp_arg cenv f args sz cont =
   match is_tailcall cont with
   | Some k ->
       comp_args comp_arg cenv args sz
-	(Kpush ::
+        (Kpush ::
          comp_fun cenv f (sz + nargs)
-	   (Kappterm(nargs, k + nargs) :: (discard_dead_code cont)))
+           (Kappterm(nargs, k + nargs) :: (discard_dead_code cont)))
   | None ->
       if nargs <= 4 then
         comp_args comp_arg cenv args sz
           (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont)))
       else
-	let lbl,cont1 = label_code cont in
-	Kpush_retaddr lbl ::
+        let lbl,cont1 = label_code cont in
+        Kpush_retaddr lbl ::
         (comp_args comp_arg cenv args (sz + 3)
            (Kpush :: (comp_fun cenv f (sz+3+nargs) (Kapply nargs :: cont1))))
 
@@ -513,8 +513,8 @@ let rec get_alias env kn =
     | None -> kn
     | Some tps ->
        (match Cemitcodes.force tps with
-	| BCalias kn' -> get_alias env kn'
-	| _ -> kn)
+        | BCalias kn' -> get_alias env kn'
+        | _ -> kn)
 
 (* sz is the size of the local stack *)
 let rec compile_lam env cenv lam sz cont =
@@ -609,24 +609,24 @@ let rec compile_lam env cenv lam sz cont =
         in
         let lbl,fcode = label_code fcode in
         lbl_types.(i) <- lbl;
-	fun_code := [Ksequence(fcode,!fun_code)]
+        fun_code := [Ksequence(fcode,!fun_code)]
       done;
       (* Compiling bodies *)
       for i = 0 to ndef - 1 do
         let params,body = decompose_Llam bodies.(i) in
         let arity = Array.length params in
-	let env_body = comp_env_fix ndef i arity rfv in
+        let env_body = comp_env_fix ndef i arity rfv in
         let cont1 =
           ensure_stack_capacity (compile_lam env env_body body arity) [Kreturn arity]
         in
-	let lbl = Label.create () in
-	lbl_bodies.(i) <- lbl;
-	let fcode =  add_grabrec rec_args.(i) arity lbl cont1 in
-	fun_code := [Ksequence(fcode,!fun_code)]
+        let lbl = Label.create () in
+        lbl_bodies.(i) <- lbl;
+        let fcode =  add_grabrec rec_args.(i) arity lbl cont1 in
+        fun_code := [Ksequence(fcode,!fun_code)]
       done;
       let fv = !rfv in
       compile_fv cenv fv.fv_rev sz
-	(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
+        (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
 
 
   | Lcofix(init, (_decl,types,bodies)) ->
@@ -642,27 +642,27 @@ let rec compile_lam env cenv lam sz cont =
         in
         let lbl,fcode = label_code fcode in
         lbl_types.(i) <- lbl;
-	fun_code := [Ksequence(fcode,!fun_code)]
+        fun_code := [Ksequence(fcode,!fun_code)]
       done;
       (* Compiling bodies *)
       for i = 0 to ndef - 1 do
         let params,body = decompose_Llam bodies.(i) in
         let arity = Array.length params in
-	let env_body = comp_env_cofix ndef arity rfv in
-	let lbl = Label.create () in
+        let env_body = comp_env_cofix ndef arity rfv in
+        let lbl = Label.create () in
         let comp arity =
           (* 4 stack slots are needed to update the cofix when forced *)
           set_max_stack_size (arity + 4);
           compile_lam env env_body body (arity+1) (cont_cofix arity)
         in
-	let cont = ensure_stack_capacity comp arity in
-	lbl_bodies.(i) <- lbl;
-	fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)];
+        let cont = ensure_stack_capacity comp arity in
+        lbl_bodies.(i) <- lbl;
+        fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)];
       done;
       let fv = !rfv in
       set_max_stack_size (sz + fv.size + ndef + 2);
       compile_fv cenv fv.fv_rev sz
-	(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
+        (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
 
   | Lif(t, bt, bf) ->
       let branch, cont = make_branch cont in
@@ -686,7 +686,7 @@ let rec compile_lam env cenv lam sz cont =
       let nblock = min nallblock (Obj.last_non_constant_constructor_tag + 1) in
       let lbl_blocks = Array.make nblock Label.no in
       let neblock = max 0 (nallblock - Obj.last_non_constant_constructor_tag) in
-      let lbl_eblocks = Array.make neblock Label.no in 
+      let lbl_eblocks = Array.make neblock Label.no in
       let branch1, cont = make_branch cont in
       (* Compilation of the return type *)
       let fcode =
@@ -708,7 +708,7 @@ let rec compile_lam env cenv lam sz cont =
       let c = ref cont in
       (* Perform the extra match if needed (too many block constructors) *)
       if neblock <> 0 then begin
-        let lbl_b, code_b = 
+        let lbl_b, code_b =
           label_code (
             Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
         lbl_blocks.(Obj.last_non_constant_constructor_tag) <- lbl_b;
@@ -756,17 +756,17 @@ let rec compile_lam env cenv lam sz cont =
      (* Compiling branch for accumulators *)
       let lbl_accu, code_accu =
         set_max_stack_size (sz+3);
-	label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch :: !c)
+        label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch :: !c)
       in
       lbl_blocks.(0) <- lbl_accu;
 
       c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: code_accu;
       let code_sw =
- 	match branch1 with
+        match branch1 with
         (* spiwack : branch1 can't be a lbl anymore it's a Branch instead
-	| Klabel lbl -> Kpush_retaddr lbl ::  !c *)
+        | Klabel lbl -> Kpush_retaddr lbl ::  !c *)
         | Kbranch lbl -> Kpush_retaddr lbl ::  !c
-	| _ -> !c
+        | _ -> !c
       in
       compile_lam env cenv a sz code_sw
 
@@ -885,13 +885,13 @@ let compile_constant_body ~fail_on_error env univs = function
       let body = Mod_subst.force_constr sb in
       let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in
       match kind body with
-	| Const (kn',u) when is_univ_copy instance_size u ->
-	    (* we use the canonical name of the constant*)
-	    let con= Constant.make1 (Constant.canonical kn') in
-	      Some (BCalias (get_alias env con))
-	| _ ->
+        | Const (kn',u) when is_univ_copy instance_size u ->
+            (* we use the canonical name of the constant*)
+            let con= Constant.make1 (Constant.canonical kn') in
+              Some (BCalias (get_alias env con))
+        | _ ->
             let res = compile ~fail_on_error ~universes:instance_size env body in
-	      Option.map (fun x -> BCdefined (to_memory x)) res
+              Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
 
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 814902a554..38c1c45a85 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -16,7 +16,7 @@ open Environ
 
 (** Should only be used for monomorphic terms *)
 val compile : fail_on_error:bool ->
-	      ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
+              ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
 (** init, fun, fv *)
 
 val compile_constant_body : fail_on_error:bool ->
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 5e82cef810..4e22421f56 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -64,14 +64,14 @@ type patches = {
   reloc_infos : (reloc_info * int array) array;
 }
 
-let patch_char4 buff pos c1 c2 c3 c4 = 
+let patch_char4 buff pos c1 c2 c3 c4 =
   Bytes.unsafe_set buff pos       c1;
   Bytes.unsafe_set buff (pos + 1) c2;
   Bytes.unsafe_set buff (pos + 2) c3;
-  Bytes.unsafe_set buff (pos + 3) c4 
-  
+  Bytes.unsafe_set buff (pos + 3) c4
+
 let patch1 buff pos n =
-  patch_char4 buff pos 
+  patch_char4 buff pos
     (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8))  (Char.unsafe_chr (n asr 16))
     (Char.unsafe_chr (n asr 24))
 
@@ -116,9 +116,9 @@ let out_word env b1 b2 b3 b4 =
       if len <= Sys.max_string_length / 2
       then 2 * len
       else
-	if len = Sys.max_string_length
-	then invalid_arg "String.create"  (* Pas la bonne exception .... *)
-	else Sys.max_string_length in
+        if len = Sys.max_string_length
+        then invalid_arg "String.create"  (* Pas la bonne exception .... *)
+        else Sys.max_string_length in
     let new_buffer = Bytes.create new_len in
     Bytes.blit env.out_buffer 0 new_buffer 0 len;
     env.out_buffer <- new_buffer
@@ -359,9 +359,9 @@ let emit_instr env = function
 (* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *)
 
 let rec emit env insns remaining = match insns with
-  | [] -> 
-     (match remaining with 
-       [] -> () 
+  | [] ->
+     (match remaining with
+       [] -> ()
      | (first::rest) -> emit env first rest)
   (* Peephole optimizations *)
   | Kpush :: Kacc n :: c ->
diff --git a/kernel/constr.ml b/kernel/constr.ml
index b60b2d6d04..15e5c512ed 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -16,7 +16,7 @@
 (* Optimization of substitution functions by Chet Murthy *)
 (* Optimization of lifting functions by Bruno Barras, Mar 1997 *)
 (* Hash-consing by Bruno Barras in Feb 1998 *)
-(* Restructuration of Coq of the type-checking kernel by Jean-Christophe 
+(* Restructuration of Coq of the type-checking kernel by Jean-Christophe
    Filliâtre, 1999 *)
 (* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *)
 (* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
@@ -924,7 +924,7 @@ let equal n m = eq_constr 0 m n (* to avoid tracing a recursive fun *)
 
 let eq_constr_univs univs m n =
   if m == n then true
-  else 
+  else
     let eq_universes _ _ = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = s1 == s2 || UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
     let rec eq_constr' nargs m n =
@@ -933,11 +933,11 @@ let eq_constr_univs univs m n =
 
 let leq_constr_univs univs m n =
   if m == n then true
-  else 
+  else
     let eq_universes _ _ = UGraph.check_eq_instances univs in
-    let eq_sorts s1 s2 = s1 == s2 || 
+    let eq_sorts s1 s2 = s1 == s2 ||
       UGraph.check_eq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
-    let leq_sorts s1 s2 = s1 == s2 || 
+    let leq_sorts s1 s2 = s1 == s2 ||
       UGraph.check_leq univs (Sorts.univ_of_sort s1) (Sorts.univ_of_sort s2) in
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
@@ -949,17 +949,17 @@ let leq_constr_univs univs m n =
 
 let eq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
-  else 
+  else
     let cstrs = ref Constraint.empty in
     let eq_universes _ _ = UGraph.check_eq_instances univs in
-    let eq_sorts s1 s2 = 
+    let eq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
       else
-	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if UGraph.check_eq univs u1 u2 then true
-	else
-	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-	   true)
+        let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
+        if UGraph.check_eq univs u1 u2 then true
+        else
+          (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+           true)
     in
     let rec eq_constr' nargs m n =
       m == n || compare_head_gen eq_universes eq_sorts eq_constr' nargs m n
@@ -969,23 +969,23 @@ let eq_constr_univs_infer univs m n =
 
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
-  else 
+  else
     let cstrs = ref Constraint.empty in
     let eq_universes _ _ l l' = UGraph.check_eq_instances univs l l' in
-    let eq_sorts s1 s2 = 
+    let eq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
       else
-	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if UGraph.check_eq univs u1 u2 then true
-	else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-	      true)
+        let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
+        if UGraph.check_eq univs u1 u2 then true
+        else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+              true)
     in
-    let leq_sorts s1 s2 = 
+    let leq_sorts s1 s2 =
       if Sorts.equal s1 s2 then true
-      else 
-	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if UGraph.check_leq univs u1 u2 then true
-	else
+      else
+        let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
+        if UGraph.check_leq univs u1 u2 then true
+        else
           (try let c, _ = UGraph.enforce_leq_alg u1 u2 univs in
             cstrs := Univ.Constraint.union c !cstrs;
             true
@@ -1183,54 +1183,54 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
   let rec hash_term t =
     match t with
       | Var i ->
-	(Var (sh_id i), combinesmall 1 (Id.hash i))
+        (Var (sh_id i), combinesmall 1 (Id.hash i))
       | Sort s ->
-	(Sort (sh_sort s), combinesmall 2 (Sorts.hash s))
+        (Sort (sh_sort s), combinesmall 2 (Sorts.hash s))
       | Cast (c, k, t) ->
-	let c, hc = sh_rec c in
-	let t, ht = sh_rec t in
-	(Cast (c, k, t), combinesmall 3 (combine3 hc (hash_cast_kind k) ht))
+        let c, hc = sh_rec c in
+        let t, ht = sh_rec t in
+        (Cast (c, k, t), combinesmall 3 (combine3 hc (hash_cast_kind k) ht))
       | Prod (na,t,c) ->
-	let t, ht = sh_rec t
-	and c, hc = sh_rec c in
+        let t, ht = sh_rec t
+        and c, hc = sh_rec c in
         (Prod (sh_na na, t, c), combinesmall 4 (combine3 (hash_annot Name.hash na) ht hc))
       | Lambda (na,t,c) ->
-	let t, ht = sh_rec t
-	and c, hc = sh_rec c in
+        let t, ht = sh_rec t
+        and c, hc = sh_rec c in
         (Lambda (sh_na na, t, c), combinesmall 5 (combine3 (hash_annot Name.hash na) ht hc))
       | LetIn (na,b,t,c) ->
-	let b, hb = sh_rec b in
-	let t, ht = sh_rec t in
-	let c, hc = sh_rec c in
+        let b, hb = sh_rec b in
+        let t, ht = sh_rec t in
+        let c, hc = sh_rec c in
         (LetIn (sh_na na, b, t, c), combinesmall 6 (combine4 (hash_annot Name.hash na) hb ht hc))
       | App (c,l) ->
-	let c, hc = sh_rec c in
-	let l, hl = hash_term_array l in
-	(App (c,l), combinesmall 7 (combine hl hc))
+        let c, hc = sh_rec c in
+        let l, hl = hash_term_array l in
+        (App (c,l), combinesmall 7 (combine hl hc))
       | Evar (e,l) ->
-	let l, hl = hash_term_array l in
-	(Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
+        let l, hl = hash_term_array l in
+        (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
       | Const (c,u) ->
-	let c' = sh_con c in
-	let u', hu = sh_instance u in
-	(Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu))
+        let c' = sh_con c in
+        let u', hu = sh_instance u in
+        (Const (c', u'), combinesmall 9 (combine (Constant.SyntacticOrd.hash c) hu))
       | Ind (ind,u) ->
-	let u', hu = sh_instance u in
-	(Ind (sh_ind ind, u'), 
-	 combinesmall 10 (combine (ind_syntactic_hash ind) hu))
+        let u', hu = sh_instance u in
+        (Ind (sh_ind ind, u'),
+         combinesmall 10 (combine (ind_syntactic_hash ind) hu))
       | Construct (c,u) ->
-	let u', hu = sh_instance u in
-	(Construct (sh_construct c, u'),
-	 combinesmall 11 (combine (constructor_syntactic_hash c) hu))
+        let u', hu = sh_instance u in
+        (Construct (sh_construct c, u'),
+         combinesmall 11 (combine (constructor_syntactic_hash c) hu))
       | Case (ci,p,c,bl) ->
-	let p, hp = sh_rec p
-	and c, hc = sh_rec c in
-	let bl,hbl = hash_term_array bl in
+        let p, hp = sh_rec p
+        and c, hc = sh_rec c in
+        let bl,hbl = hash_term_array bl in
         let hbl = combine (combine hc hp) hbl in
-	(Case (sh_ci ci, p, c, bl), combinesmall 12 hbl)
+        (Case (sh_ci ci, p, c, bl), combinesmall 12 hbl)
       | Fix (ln,(lna,tl,bl)) ->
         let bl,hbl = hash_term_array bl in
-	let tl,htl = hash_term_array tl in
+        let tl,htl = hash_term_array tl in
         let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in
         let fold accu na = combine (hash_annot Name.hash na) accu in
         let hna = Array.fold_left fold 0 lna in
@@ -1238,16 +1238,16 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
         (Fix (ln,(lna,tl,bl)), combinesmall 13 h)
       | CoFix(ln,(lna,tl,bl)) ->
         let bl,hbl = hash_term_array bl in
-	let tl,htl = hash_term_array tl in
+        let tl,htl = hash_term_array tl in
         let () = Array.iteri (fun i x -> Array.unsafe_set lna i (sh_na x)) lna in
         let fold accu na = combine (hash_annot Name.hash na) accu in
         let hna = Array.fold_left fold 0 lna in
         let h = combine3 hna hbl htl in
         (CoFix (ln,(lna,tl,bl)), combinesmall 14 h)
       | Meta n ->
-	(t, combinesmall 15 n)
+        (t, combinesmall 15 n)
       | Rel n ->
-	(t, combinesmall 16 n)
+        (t, combinesmall 16 n)
       | Proj (p,c) ->
         let c, hc = sh_rec c in
         let p' = Projection.hcons p in
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 4f8d682e42..d4af1149c2 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -140,13 +140,13 @@ val mkConstructUi : pinductive * int -> constr
 val mkRef : GlobRef.t Univ.puniverses -> constr
 
 (** Constructs a destructor of inductive type.
-    
-    [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] 
+
+    [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac]
     presented as describe in [ci].
 
     [p] structure is [fun args x -> "return clause"]
 
-    [ac]{^ ith} element is ith constructor case presented as 
+    [ac]{^ ith} element is ith constructor case presented as
     {e lambda construct_args (without params). case_term } *)
 val mkCase : case_info * constr * constr * constr array -> constr
 
@@ -188,10 +188,10 @@ val mkFix : fixpoint -> constr
 
 (** If [funnames = [|f1,.....fn|]]
       [typarray = [|t1,...tn|]]
-      [bodies   = [b1,.....bn]] 
+      [bodies   = [b1,.....bn]]
    then [mkCoFix (i, (funnames, typarray, bodies))]
    constructs the ith function of the block
-   
+
     [CoFixpoint f1 = b1
      with       f2 = b2
      ...
@@ -365,7 +365,7 @@ val equal : constr -> constr -> bool
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr UGraph.check_function
 
-(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
     alpha, casts, application grouping and the universe inequalities in [u]. *)
 val leq_constr_univs : constr UGraph.check_function
 
@@ -373,7 +373,7 @@ val leq_constr_univs : constr UGraph.check_function
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained
 
-(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo
     alpha, casts, application grouping and the universe inequalities in [u]. *)
 val leq_constr_univs_infer : UGraph.t -> constr -> constr -> bool Univ.constrained
 
diff --git a/kernel/context.ml b/kernel/context.ml
index 2ef750ad69..7e394da2ed 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -74,7 +74,7 @@ struct
     let get_value = function
       | LocalAssum _ -> None
       | LocalDef (_,v,_) -> Some v
-                                 
+
     (** Return the type of the name bound by a given declaration. *)
     let get_type = function
       | LocalAssum (_,ty)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 918dc8c928..4887e70cdb 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -18,7 +18,7 @@ val empty : oracle
    If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : ('a -> Constant.t) -> oracle -> bool -> 
+val oracle_order : ('a -> Constant.t) -> oracle -> bool ->
   'a tableKey -> 'a tableKey -> bool
 
 (** Priority for the expansion of constant in the conversion test.
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index fae06f7163..9d7387c7ad 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -91,25 +91,25 @@ let expmod_constr cache modlist c =
   let rec substrec c =
     match kind c with
       | Case (ci,p,t,br) ->
-	  Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br))
+          Constr.map substrec (mkCase (update_case_info ci modlist,p,t,br))
 
       | Ind (ind,u) ->
-	  (try
-	    share_univs (IndRef ind) u modlist
-	   with
-	    | Not_found -> Constr.map substrec c)
+          (try
+            share_univs (IndRef ind) u modlist
+           with
+            | Not_found -> Constr.map substrec c)
 
       | Construct (cstr,u) ->
-	  (try
-	     share_univs (ConstructRef cstr) u modlist
-	   with
-	    | Not_found -> Constr.map substrec c)
+          (try
+             share_univs (ConstructRef cstr) u modlist
+           with
+            | Not_found -> Constr.map substrec c)
 
       | Const (cst,u) ->
-	  (try
-	    share_univs (ConstRef cst) u modlist
-	   with
-	    | Not_found -> Constr.map substrec c)
+          (try
+            share_univs (ConstRef cst) u modlist
+           with
+            | Not_found -> Constr.map substrec c)
 
       | Proj (p, c') ->
         let map cst npars =
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index cbffdc731e..978c2c9f57 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -135,12 +135,12 @@ let rec slot_for_getglobal env kn =
       match cb.const_body_code with
       | None -> set_global (val_of_constant kn)
       | Some code ->
-	 match Cemitcodes.force code with
-	 | BCdefined(code,pl,fv) ->
+         match Cemitcodes.force code with
+         | BCdefined(code,pl,fv) ->
            let v = eval_to_patch env (code,pl,fv) in
            set_global v
-	 | BCalias kn' -> slot_for_getglobal env kn'
-	 | BCconstant -> set_global (val_of_constant kn)
+         | BCalias kn' -> slot_for_getglobal env kn'
+         | BCconstant -> set_global (val_of_constant kn)
     in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (CEphemeron.create pos);
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 44676c9da5..9fd10b32e6 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -25,7 +25,7 @@ type engagement = set_predicativity
     and constants hiding inductives are implicitly polymorphic when
     applied to parameters, on the universes appearing in the whnf of
     their parameters and their conclusion, in a template style.
-    
+
     In truly universe polymorphic mode, we always use RegularArity.
 *)
 
@@ -34,7 +34,7 @@ type template_arity = {
   template_level : Univ.Universe.t;
 }
 
-type ('a, 'b) declaration_arity = 
+type ('a, 'b) declaration_arity =
   | RegularArity of 'a
   | TemplateArity of 'b
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 7225671a1e..35185b6a5e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -31,14 +31,14 @@ let safe_flags oracle = {
 
 (** {6 Arities } *)
 
-let subst_decl_arity f g sub ar = 
+let subst_decl_arity f g sub ar =
   match ar with
-  | RegularArity x -> 
-    let x' = f sub x in 
+  | RegularArity x ->
+    let x' = f sub x in
       if x' == x then ar
       else RegularArity x'
-  | TemplateArity x -> 
-    let x' = g sub x in 
+  | TemplateArity x ->
+    let x' = g sub x in
       if x' == x then ar
       else TemplateArity x'
 
@@ -197,7 +197,7 @@ let subst_wf_paths sub p = Rtree.Smart.map (subst_recarg sub) p
 
 let subst_regular_ind_arity sub s =
   let uar' = subst_mps sub s.mind_user_arity in
-    if uar' == s.mind_user_arity then s 
+    if uar' == s.mind_user_arity then s
     else { mind_user_arity = uar'; mind_sort = s.mind_sort }
 
 let subst_template_ind_arity _sub s = s
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 046ea86872..b50c3ebbc3 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -87,7 +87,7 @@ type 'a opaque_entry = {
 
 type inline = int option (* inlining level, None for no inlining *)
 
-type parameter_entry = 
+type parameter_entry =
     Id.Set.t option * types in_universes_entry * inline
 
 type primitive_entry = {
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2bee2f7a8e..f04863386f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -259,7 +259,7 @@ let set_oracle env o =
 let engagement env = env.env_stratification.env_engagement
 let typing_flags env = env.env_typing_flags
 
-let is_impredicative_set env = 
+let is_impredicative_set env =
   match engagement env with
   | ImpredicativeSet -> true
   | _ -> false
@@ -312,11 +312,11 @@ let fold_rel_context f env ~init =
     match match_rel_context_val env.env_rel_context with
     | None -> init
     | Some (rd, _, rc) ->
-	let env =
-	  { env with
-	    env_rel_context = rc;
-	    env_nb_rel = env.env_nb_rel - 1 } in
-	f env rd (fold_right env)
+        let env =
+          { env with
+            env_rel_context = rc;
+            env_nb_rel = env.env_nb_rel - 1 } in
+        f env rd (fold_right env)
   in fold_right env
 
 (* Named context *)
@@ -376,9 +376,9 @@ let fold_named_context f env ~init =
     match match_named_context_val env.env_named_context with
     | None -> init
     | Some (d, _v, rem) ->
-	let env =
-	  reset_with_named_context rem env in
-	f env d (fold_right env)
+        let env =
+          reset_with_named_context rem env in
+        f env d (fold_right env)
   in fold_right env
 
 let fold_named_context_reverse f ~init env =
@@ -390,7 +390,7 @@ let fold_named_context_reverse f ~init env =
 let map_universes f env =
   let s = env.env_stratification in
     { env with env_stratification =
-	 { s with env_universes = f s.env_universes } }
+         { s with env_universes = f s.env_universes } }
 
 let add_constraints c env =
   if Univ.Constraint.is_empty c then env
@@ -405,10 +405,10 @@ let push_constraints_to_env (_,univs) env =
 let add_universes ~lbound ~strict ctx g =
   let g = Array.fold_left
             (fun g v -> UGraph.add_universe ~lbound ~strict v g)
-	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+            g (Univ.Instance.to_array (Univ.UContext.instance ctx))
   in
     UGraph.merge_constraints (Univ.UContext.constraints ctx) g
-			   
+
 let push_context ?(strict=false) ctx env =
   map_universes (add_universes ~lbound:(universes_lbound env) ~strict ctx) env
 
@@ -416,7 +416,7 @@ let add_universes_set ~lbound ~strict ctx g =
   let g = Univ.LSet.fold
             (* Be lenient, module typing reintroduces universes and constraints due to includes *)
             (fun v g -> try UGraph.add_universe ~lbound ~strict v g with UGraph.AlreadyDeclared -> g)
-	    (Univ.ContextSet.levels ctx) g
+            (Univ.ContextSet.levels ctx) g
   in UGraph.merge_constraints (Univ.ContextSet.constraints ctx) g
 
 let push_context_set ?(strict=false) ctx env =
@@ -514,8 +514,8 @@ let constant_value_and_type env (kn, u) =
   in
   b', subst_instance_constr u cb.const_type, cst
 
-(* These functions should be called under the invariant that [env] 
-   already contains the constraints corresponding to the constant 
+(* These functions should be called under the invariant that [env]
+   already contains the constraints corresponding to the constant
    application. *)
 
 (* constant_type gives the type of a constant *)
@@ -526,9 +526,9 @@ let constant_type_in env (kn,u) =
 let constant_value_in env (kn,u) =
   let cb = lookup_constant kn env in
   match cb.const_body with
-    | Def l_body -> 
+    | Def l_body ->
       let b = Mod_subst.force_constr l_body in
-	subst_instance_constr u b
+        subst_instance_constr u b
     | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
     | Undef _ -> raise (NotEvaluableConst NoBody)
     | Primitive p -> raise (NotEvaluableConst (IsPrimitive p))
@@ -595,7 +595,7 @@ let template_checked_ind (mind,_i) env =
   (lookup_mind mind env).mind_typing_flags.check_template
 
 let template_polymorphic_ind (mind,i) env =
-  match (lookup_mind mind env).mind_packets.(i).mind_arity with 
+  match (lookup_mind mind env).mind_packets.(i).mind_arity with
   | TemplateArity _ -> true
   | RegularArity _ -> false
 
@@ -608,7 +608,7 @@ let template_polymorphic_variables (mind,i) env =
 let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
   else template_polymorphic_ind ind env
-  
+
 let add_mind_key kn (_mind, _ as mind_key) env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.Globals.inductives in
   let new_globals =
@@ -749,11 +749,11 @@ let apply_to_hyp ctxt id f =
   let rec aux rtail ctxt =
     match match_named_context_val ctxt with
     | Some (d, v, ctxt) ->
-	if Id.equal (get_id d) id then
+        if Id.equal (get_id d) id then
           push_named_context_val_val (f ctxt.env_named_ctx d rtail) v ctxt
-	else
-	  let ctxt' = aux (d::rtail) ctxt in
-	  push_named_context_val_val d v ctxt'
+        else
+          let ctxt' = aux (d::rtail) ctxt in
+          push_named_context_val_val d v ctxt'
     | None -> raise Hyp_not_found
   in aux [] ctxt
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 782ea1c666..257bd43083 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -127,7 +127,7 @@ val push_rel         : Constr.rel_declaration -> env -> env
 val push_rel_context : Constr.rel_context -> env -> env
 val push_rec_types   : rec_declaration -> env -> env
 
-(** Looks up in the context of local vars referred by indice ([rel_context]) 
+(** Looks up in the context of local vars referred by indice ([rel_context])
    raises [Not_found] if the index points out of the context *)
 val lookup_rel    : int -> env -> Constr.rel_declaration
 val lookup_rel_val : int -> env -> lazy_val
@@ -160,7 +160,7 @@ val push_named_context_val  :
 
 
 
-(** Looks up in the context of local vars referred by names ([named_context]) 
+(** Looks up in the context of local vars referred by names ([named_context])
    raises [Not_found] if the Id.t is not found *)
 
 val lookup_named     : variable -> env -> Constr.named_declaration
@@ -200,7 +200,7 @@ val add_constant_key : Constant.t -> Opaqueproof.opaque constant_body -> link_in
   env -> env
 val lookup_constant_key :  Constant.t -> env -> constant_key
 
-(** Looks up in the context of global constant names 
+(** Looks up in the context of global constant names
    raises an anomaly if the required path is not found *)
 val lookup_constant    : Constant.t -> env -> Opaqueproof.opaque constant_body
 val evaluable_constant : Constant.t -> env -> bool
@@ -227,14 +227,14 @@ exception NotEvaluableConst of const_evaluation_result
 
 val constant_type : env -> Constant.t puniverses -> types constrained
 
-val constant_value_and_type : env -> Constant.t puniverses -> 
+val constant_value_and_type : env -> Constant.t puniverses ->
   constr option * types * Univ.Constraint.t
-(** The universe context associated to the constant, empty if not 
+(** The universe context associated to the constant, empty if not
     polymorphic *)
 val constant_context : env -> Constant.t -> Univ.AUContext.t
 
-(* These functions should be called under the invariant that [env] 
-   already contains the constraints corresponding to the constant 
+(* These functions should be called under the invariant that [env]
+   already contains the constraints corresponding to the constant
    application. *)
 val constant_value_in : env -> Constant.t puniverses -> constr
 val constant_type_in : env -> Constant.t puniverses -> types
@@ -255,7 +255,7 @@ val lookup_mind_key : MutInd.t -> env -> mind_key
 val add_mind_key : MutInd.t -> mind_key -> env -> env
 val add_mind : MutInd.t -> mutual_inductive_body -> env -> env
 
-(** Looks up in the context of global inductive names 
+(** Looks up in the context of global inductive names
    raises an anomaly if the required path is not found *)
 val lookup_mind : MutInd.t -> env -> mutual_inductive_body
 
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 400f91d302..a1a5b5251a 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -11,7 +11,7 @@
 (** Explicit substitutions *)
 
 (** {6 Explicit substitutions } *)
-(** Explicit substitutions of type ['a]. 
+(** Explicit substitutions of type ['a].
     - ESID(n)             = %n END   bounded identity
     - CONS([|t1..tn|],S)  = (S.t1...tn)    parallel substitution
         (beware of the order: indice 1 is substituted by tn)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index aa3ef715db..750ac86908 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -74,18 +74,18 @@ let explain_ind_err id ntyp env nparamsctxt c err =
   let (_lparams,c') = mind_extract_params nparamsctxt c in
   match err with
     | LocalNonPos kt ->
-	raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt))))
+        raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt))))
     | LocalNotEnoughArgs kt ->
-	raise (InductiveError
-		 (NotEnoughArgs (env,c',mkRel (kt+nparamsctxt))))
+        raise (InductiveError
+                 (NotEnoughArgs (env,c',mkRel (kt+nparamsctxt))))
     | LocalNotConstructor (paramsctxt,nargs)->
         let nparams = Context.Rel.nhyps paramsctxt in
-	raise (InductiveError
-		 (NotConstructor (env,id,c',mkRel (ntyp+nparamsctxt),
+        raise (InductiveError
+                 (NotConstructor (env,id,c',mkRel (ntyp+nparamsctxt),
                                   nparams,nargs)))
     | LocalNonPar (n,i,l) ->
-	raise (InductiveError
-		 (NonPar (env,c',n,mkRel i,mkRel (l+nparamsctxt))))
+        raise (InductiveError
+                 (NonPar (env,c',n,mkRel i,mkRel (l+nparamsctxt))))
 
 let failwith_non_pos n ntypes c =
   for k = n to n + ntypes - 1 do
@@ -115,9 +115,9 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args =
       check param_index (paramdecl_index+1) paramdecls
     | _::paramdecls ->
         match kind (whd_all env params.(param_index)) with
-	  | Rel w when Int.equal w paramdecl_index ->
+          | Rel w when Int.equal w paramdecl_index ->
             check (param_index-1) (paramdecl_index+1) paramdecls
-	  | _ ->
+          | _ ->
             let paramdecl_index_in_env = paramdecl_index-n+nparamdecls+1 in
             let err =
               LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in
@@ -137,12 +137,12 @@ if Int.equal nmr 0 then 0 else
   let (lpar,_) = List.chop nmr largs in
   let rec find k index =
       function
-	  ([],_) -> nmr
-	| (_,[]) -> assert false (* |paramsctxt|>=nmr *)
-	| (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt)
-	| (p::lp,_::paramsctxt) ->
+          ([],_) -> nmr
+        | (_,[]) -> assert false (* |paramsctxt|>=nmr *)
+        | (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt)
+        | (p::lp,_::paramsctxt) ->
        ( match kind (whd_all env p) with
-	  | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt)
+          | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt)
           | _ -> k)
   in find 0 (n-1) (lpar,List.rev paramsctxt)
 
@@ -177,7 +177,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
     match kind c' with
         Prod(na,a,b) ->
           let ienv' = ienv_push_var ienv (na,a,mk_norec) in
-	  ienv_decompose_prod ienv' (n-1) b
+          ienv_decompose_prod ienv' (n-1) b
       | _ -> assert false
 
 let array_min nmr a = if Int.equal nmr 0 then 0 else
@@ -205,36 +205,36 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
     let x,largs = decompose_app (whd_all env c) in
       match kind x with
         | Prod (na,b,d) ->
-	    let () = assert (List.is_empty largs) in
+            let () = assert (List.is_empty largs) in
             (** If one of the inductives of the mutually inductive
                 block occurs in the left-hand side of a product, then
                 such an occurrence is a non-strictly-positive
                 recursive call. Occurrences in the right-hand side of
                 the product must be strictly positive.*)
             (match weaker_noccur_between env n ntypes b with
-	      | None when chkpos ->
+              | None when chkpos ->
                   failwith_non_pos_list n ntypes [b]
               | None ->
                   check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d
               | Some b ->
                   check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
-	| Rel k ->
+        | Rel k ->
             (try let (ra,rarg) = List.nth ra_env (k-1) in
             let largs = List.map (whd_all env) largs in
-	    let nmr1 =
-	      (match ra with
+            let nmr1 =
+              (match ra with
                   Mrec _ -> compute_rec_par ienv paramsctxt nmr largs
-		|  _ -> nmr)
-	    in
+                |  _ -> nmr)
+            in
               (** The case where one of the inductives of the mutually
                   inductive block occurs as an argument of another is not
                   known to be safe. So Coq rejects it. *)
-	      if chkpos &&
+              if chkpos &&
                  not (List.for_all (noccur_between n ntypes) largs)
-	      then failwith_non_pos_list n ntypes largs
-	      else (nmr1,rarg)
+              then failwith_non_pos_list n ntypes largs
+              else (nmr1,rarg)
               with Failure _ | Invalid_argument _ -> (nmr,mk_norec))
-	| Ind ind_kn ->
+        | Ind ind_kn ->
             (** If one of the inductives of the mutually inductive
                 block being defined appears in a parameter, then we
                 have a nested inductive type. The positivity is then
@@ -245,11 +245,11 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
             (** If an inductive of the mutually inductive block
                 appears in any other way, then the positivy check gives
                 up. *)
-	    if not chkpos ||
+            if not chkpos ||
               (noccur_between n ntypes x &&
                List.for_all (noccur_between n ntypes) largs)
-	    then (nmr,mk_norec)
-	    else failwith_non_pos_list n ntypes (x::largs)
+            then (nmr,mk_norec)
+            else failwith_non_pos_list n ntypes (x::largs)
 
   (** [check_positive_nested] handles the case of nested inductive
       calls, that is, when an inductive types from the mutually
@@ -270,35 +270,35 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
           allowed to appear nested in the parameters of another inductive
           type. Not in the proper indices. *)
       if chkpos && not (List.for_all (noccur_between n ntypes) auxnonrecargs) then
-	failwith_non_pos_list n ntypes auxnonrecargs;
+        failwith_non_pos_list n ntypes auxnonrecargs;
       (* Nested mutual inductive types are not supported *)
       let auxntyp = mib.mind_ntypes in
-	if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n));
-	(* The nested inductive type with parameters removed *)
-	let auxlcvect = abstract_mind_lc auxntyp auxnrecpar mip.mind_nf_lc in
-	  (* Extends the environment with a variable corresponding to
-	     the inductive def *)
-	let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),auxrecparams) in
-	  (* Parameters expressed in env' *)
-	let auxrecparams' = List.map (lift auxntyp) auxrecparams in
-	let irecargs_nmr =
-	  (** Checks that the "nesting" inductive type is covariant in
-	      the relevant parameters. In other words, that the
-	      (nested) parameters which are instantiated with
-	      inductives of the mutually inductive block occur
-	      positively in the types of the nested constructors. *)
-	  Array.map
-	    (function c ->
-	      let c' = hnf_prod_applist env' c auxrecparams' in
-	      (* skip non-recursive parameters *)
-	      let (ienv',c') = ienv_decompose_prod ienv' auxnnonrecpar c' in
-		check_constructors ienv' false nmr c')
-	    auxlcvect
-	in
-	let irecargs = Array.map snd irecargs_nmr
-	and nmr' = array_min nmr irecargs_nmr
-	in
-	  (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0))
+        if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n));
+        (* The nested inductive type with parameters removed *)
+        let auxlcvect = abstract_mind_lc auxntyp auxnrecpar mip.mind_nf_lc in
+          (* Extends the environment with a variable corresponding to
+             the inductive def *)
+        let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),auxrecparams) in
+          (* Parameters expressed in env' *)
+        let auxrecparams' = List.map (lift auxntyp) auxrecparams in
+        let irecargs_nmr =
+          (** Checks that the "nesting" inductive type is covariant in
+              the relevant parameters. In other words, that the
+              (nested) parameters which are instantiated with
+              inductives of the mutually inductive block occur
+              positively in the types of the nested constructors. *)
+          Array.map
+            (function c ->
+              let c' = hnf_prod_applist env' c auxrecparams' in
+              (* skip non-recursive parameters *)
+              let (ienv',c') = ienv_decompose_prod ienv' auxnnonrecpar c' in
+                check_constructors ienv' false nmr c')
+            auxlcvect
+        in
+        let irecargs = Array.map snd irecargs_nmr
+        and nmr' = array_min nmr irecargs_nmr
+        in
+          (nmr',(Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0))
 
   (** [check_constructors ienv check_head nmr c] checks the positivity
       condition in the type [c] of a constructor (i.e. that recursive
@@ -311,11 +311,11 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
   and check_constructors ienv check_head nmr c =
     let rec check_constr_rec (env,n,ntypes,_ra_env as ienv) nmr lrec c =
       let x,largs = decompose_app (whd_all env c) in
-	match kind x with
+        match kind x with
 
           | Prod (na,b,d) ->
-	      let () = assert (List.is_empty largs) in
-	      if not recursive && not (noccur_between n ntypes b) then
+              let () = assert (List.is_empty largs) in
+              if not recursive && not (noccur_between n ntypes b) then
                 raise (InductiveError Type_errors.BadEntry);
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
@@ -341,9 +341,9 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
       (fun id c ->
         let _,rawc = mind_extract_params nparamsctxt c in
           try
-	    check_constructors ienv true nmr rawc
+            check_constructors ienv true nmr rawc
           with IllFormedInd err ->
-	    explain_ind_err id (ntypes-i) env nparamsctxt c err)
+            explain_ind_err id (ntypes-i) env nparamsctxt c err)
       (Array.of_list lcnames) indlc
   in
   let irecargs = Array.map snd irecargs_nmr
@@ -397,7 +397,7 @@ let rel_list n m = Array.to_list (rel_vect n m)
 
 (** From a rel context describing the constructor arguments,
     build an expansion function.
-    The term built is expecting to be substituted first by 
+    The term built is expecting to be substituted first by
     a substitution of the form [params, x : ind params] *)
 let compute_projections (kn, i as ind) mib =
   let pkt = mib.mind_packets.(i) in
@@ -444,10 +444,10 @@ let compute_projections (kn, i as ind) mib =
         let t = liftn 1 j t in
         (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
            to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
-	let projty = substl letsubst t in
+        let projty = substl letsubst t in
         (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
            to [params, x:I |- t(proj1 x,..,projj x)] *)
-	let fterm = mkProj (Projection.make kn false, mkRel 1) in
+        let fterm = mkProj (Projection.make kn false, mkRel 1) in
         (i + 1, j + 1, lab :: labs, r :: rs, projty :: pbs, fterm :: letsubst)
       | Anonymous -> assert false (* checked by indTyping *)
   in
@@ -469,7 +469,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
     let nf_lc = Array.map (fun (d, b) -> (d@paramsctxt, b)) splayed_lc in
     let consnrealdecls =
       Array.map (fun (d,_) -> Context.Rel.length d)
-	splayed_lc in
+        splayed_lc in
     let consnrealargs =
       Array.map (fun (d,_) -> Context.Rel.nhyps d)
         splayed_lc in
@@ -481,14 +481,14 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
     let nconst, nblock = ref 0, ref 0 in
     let transf num =
       let arity = List.length (dest_subterms recarg).(num) in
-	if Int.equal arity 0 then
-	  let p  = (!nconst, 0) in
-	    incr nconst; p
-	else
-	  let p = (!nblock + 1, arity) in
-	    incr nblock; p
-	      (* les tag des constructeur constant commence a 0,
-		 les tag des constructeur non constant a 1 (0 => accumulator) *)
+        if Int.equal arity 0 then
+          let p  = (!nconst, 0) in
+            incr nconst; p
+        else
+          let p = (!nblock + 1, arity) in
+            incr nblock; p
+              (* les tag des constructeur constant commence a 0,
+                 les tag des constructeur non constant a 1 (0 => accumulator) *)
     in
     let rtbl = Array.init (List.length cnames) transf in
       (* Build the inductive packet *)
@@ -497,17 +497,17 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
         mind_arity_ctxt = indices @ paramsctxt;
         mind_nrealargs = Context.Rel.nhyps indices;
         mind_nrealdecls = Context.Rel.length indices;
-	mind_kelim = kelim;
-	mind_consnames = Array.of_list cnames;
-	mind_consnrealdecls = consnrealdecls;
-	mind_consnrealargs = consnrealargs;
-	mind_user_lc = lc;
-	mind_nf_lc = nf_lc;
+        mind_kelim = kelim;
+        mind_consnames = Array.of_list cnames;
+        mind_consnrealdecls = consnrealdecls;
+        mind_consnrealargs = consnrealargs;
+        mind_user_lc = lc;
+        mind_nf_lc = nf_lc;
         mind_recargs = recarg;
         mind_relevance;
         mind_nb_constant = !nconst;
-	mind_nb_args = !nblock;
-	mind_reloc_tbl = rtbl;
+        mind_nb_args = !nblock;
+        mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map3 build_one_packet names inds recargs in
   let mib =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 2966acae45..ca4fea45c5 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -52,7 +52,7 @@ let find_coinductive env c =
 
 let inductive_params (mib,_) = mib.mind_nparams
 
-let inductive_paramdecls (mib,u) = 
+let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
@@ -81,9 +81,9 @@ let instantiate_params full t u args sign =
         match (decl, largs, kind ty) with
           | (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
           | (LocalDef (_,b,_), _, LetIn(_,_,_,t))    ->
-	     (largs, (substl subs (subst_instance_constr u b))::subs, t)
-	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
-	  | _                       -> fail ())
+             (largs, (substl subs (subst_instance_constr u b))::subs, t)
+          | (_,[],_)                -> if full then fail() else ([], subs, ty)
+          | _                       -> fail ())
       sign
       ~init:(args,[],t)
   in
@@ -98,7 +98,7 @@ let full_inductive_instantiate mib u params sign =
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
   let inst_ind = constructor_instantiate mind u mib t in
    instantiate_params true inst_ind u params mib.mind_params_ctxt
-		      
+
 (************************************************************************)
 (************************************************************************)
 
@@ -211,7 +211,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps =
       then raise (SingletonInductiveBecomesProp mip.mind_typename);
       Term.mkArity (List.rev ctx,s)
 
-let type_of_inductive env pind = 
+let type_of_inductive env pind =
   type_of_inductive_gen env pind [||]
 
 let constrained_type_of_inductive env ((mib,_mip),u as pind) =
@@ -292,7 +292,7 @@ let get_instantiated_arity (_ind,u) (mib,mip) params =
 let elim_sort (_,mip) = mip.mind_kelim
 
 let is_private (mib,_) = mib.mind_private = Some true
-let is_primitive_record (mib,_) = 
+let is_primitive_record (mib,_) =
   match mib.mind_record with
   | PrimRecord _ -> true
   | NotRecord | FakeRecord -> false
@@ -325,20 +325,20 @@ let is_correct_arity env c pj ind specif params =
       (* The last Prod domain is the type of the scrutinee *)
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
          let env' = push_rel (LocalAssum (na1,a1)) env in
-	 let ksort = match kind (whd_all env' a2) with
-	 | Sort s -> Sorts.family s
-	 | _ -> raise (LocalArity None) in
-	 let dep_ind = build_dependent_inductive ind specif params in
-	 let _ =
+         let ksort = match kind (whd_all env' a2) with
+         | Sort s -> Sorts.family s
+         | _ -> raise (LocalArity None) in
+         let dep_ind = build_dependent_inductive ind specif params in
+         let _ =
            try conv env a1 dep_ind
            with NotConvertible -> raise (LocalArity None) in
-	   check_allowed_sort ksort specif
+           check_allowed_sort ksort specif
       | _, (LocalDef _ as d)::ar' ->
-	  srec (push_rel d env) (lift 1 pt') ar'
+          srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
-	  raise (LocalArity None)
+          raise (LocalArity None)
   in
-  try srec env pj.uj_type (List.rev arsign) 
+  try srec env pj.uj_type (List.rev arsign)
   with LocalArity kinds ->
     error_elim_arity env ind c pj kinds
 
@@ -517,10 +517,10 @@ let push_fix_renv renv (_,v,_ as recdef) =
 (* Definition and manipulation of the stack *)
 type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
 
-let push_stack_closures renv l stack = 
+let push_stack_closures renv l stack =
   List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack
 
-let push_stack_args l stack = 
+let push_stack_args l stack =
   List.fold_right (fun h b -> (SArg h)::b) l stack
 
 (******************************)
@@ -540,7 +540,7 @@ let match_inductive ind ra =
    [branches_specif renv c_spec ci] returns an array of x_s specs knowing
    c_spec. *)
 let branches_specif renv c_spec ci =
-  let car = 
+  let car =
     (* We fetch the regular tree associated to the inductive of the match.
        This is just to get the number of constructors (and constructor
        arities) that fit the match branches without forcing c_spec.
@@ -551,16 +551,16 @@ let branches_specif renv c_spec ci =
       Array.map List.length v in
     Array.mapi
       (fun i nca -> (* i+1-th cstructor has arity nca *)
-	 let lvra = lazy 
-	   (match Lazy.force c_spec with
-		Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
-		  let vra = Array.of_list (dest_subterms t).(i) in
-		  assert (Int.equal nca (Array.length vra));
-		  Array.map spec_of_tree vra
-	      | Dead_code -> Array.make nca Dead_code
-	      | _ -> Array.make nca Not_subterm) in
-	 List.init nca (fun j -> lazy (Lazy.force lvra).(j)))
-      car 
+         let lvra = lazy
+           (match Lazy.force c_spec with
+                Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
+                  let vra = Array.of_list (dest_subterms t).(i) in
+                  assert (Int.equal nca (Array.length vra));
+                  Array.map spec_of_tree vra
+              | Dead_code -> Array.make nca Dead_code
+              | _ -> Array.make nca Not_subterm) in
+         List.init nca (fun j -> lazy (Lazy.force lvra).(j)))
+      car
 
 let check_inductive_codomain env p =
   let absctx, ar = dest_lam_assum env p in
@@ -615,7 +615,7 @@ let abstract_mind_lc ntyps npars lc =
   else
     let make_abs =
       List.init ntyps
-	(function i -> lambda_implicit_lift npars (mkRel (i+1)))
+        (function i -> lambda_implicit_lift npars (mkRel (i+1)))
     in
     Array.map (substl make_abs) lc
 
@@ -639,9 +639,9 @@ let get_recargs_approx env tree ind args =
        (* When the inferred tree allows it, we consider that we have a potential
        nested inductive type *)
        begin match dest_recarg tree with
-	     | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
-			   build_recargs_nested ienv tree (ind_kn, largs)
-	     | _ -> mk_norec
+             | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+                           build_recargs_nested ienv tree (ind_kn, largs)
+             | _ -> mk_norec
        end
     | _err ->
        mk_norec
@@ -656,7 +656,7 @@ let get_recargs_approx env tree ind args =
     let (lpar,_) = List.chop auxnpar largs in
     let auxntyp = mib.mind_ntypes in
     (* Extends the environment with a variable corresponding to
-	     the inductive def *)
+             the inductive def *)
     let (env',_ as ienv') = ienv_push_inductive ienv ((mind,u),lpar) in
     (* Parameters expressed in env' *)
     let lpar' = List.map (lift auxntyp) lpar in
@@ -672,11 +672,11 @@ let get_recargs_approx env tree ind args =
       let auxlcvect = abstract_mind_lc auxntyp auxnpar specif.mind_nf_lc in
       let paths = Array.mapi
         (fun k c ->
-	 let c' = hnf_prod_applist env' c lpar' in
-	 (* skip non-recursive parameters *)
-	 let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in
-	 build_recargs_constructors ienv' trees.(j).(k) c')
-	auxlcvect
+         let c' = hnf_prod_applist env' c lpar' in
+         (* skip non-recursive parameters *)
+         let (ienv',c') = ienv_decompose_prod ienv' nonrecpar c' in
+         build_recargs_constructors ienv' trees.(j).(k) c')
+        auxlcvect
       in
       mk_paths (Imbr (mind,j)) paths
     in
@@ -686,10 +686,10 @@ let get_recargs_approx env tree ind args =
   and build_recargs_constructors ienv trees c =
     let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c =
       let x,largs = decompose_app (whd_all env c) in
-	match kind x with
+        match kind x with
 
           | Prod (na,b,d) ->
-	     let () = assert (List.is_empty largs) in
+             let () = assert (List.is_empty largs) in
              let recarg = build_recargs ienv (List.hd trees) b in
              let ienv' = ienv_push_var ienv (na,b,mk_norec) in
              recargs_constr_rec ienv' (List.tl trees) (recarg::lrec) d
@@ -718,12 +718,12 @@ let restrict_spec env spec p =
   match kind i with
   | Ind i ->
      begin match spec with
-	   | Dead_code -> spec
-	   | Subterm(st,tree) ->
-	      let recargs = get_recargs_approx env tree i args in
-	      let recargs = inter_wf_paths tree recargs in
-	      Subterm(st,recargs)
-	   | _ -> assert false
+           | Dead_code -> spec
+           | Subterm(st,tree) ->
+              let recargs = get_recargs_approx env tree i args in
+              let recargs = inter_wf_paths tree recargs in
+              Subterm(st,recargs)
+           | _ -> assert false
      end
   | _ -> Not_subterm
 
@@ -741,25 +741,25 @@ let rec subterm_specif renv stack t =
     | Case (ci,p,c,lbr) ->
        let stack' = push_stack_closures renv l stack in
        let cases_spec =
-	 branches_specif renv (lazy_subterm_specif renv [] c) ci
+         branches_specif renv (lazy_subterm_specif renv [] c) ci
        in
        let stl =
-	 Array.mapi (fun i br' ->
-		     let stack_br = push_stack_args (cases_spec.(i)) stack' in
-		     subterm_specif renv stack_br br')
-		    lbr in
+         Array.mapi (fun i br' ->
+                     let stack_br = push_stack_args (cases_spec.(i)) stack' in
+                     subterm_specif renv stack_br br')
+                    lbr in
        let spec = subterm_spec_glb stl in
        restrict_spec renv.env spec p
 
     | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
       (* when proving that the fixpoint f(x)=e is less than n, it is enough
-	 to prove that e is less than n assuming f is less than n
-	 furthermore when f is applied to a term which is strictly less than
-	 n, one may assume that x itself is strictly less than n
+         to prove that e is less than n assuming f is less than n
+         furthermore when f is applied to a term which is strictly less than
+         n, one may assume that x itself is strictly less than n
       *)
     if not (check_inductive_codomain renv.env typarray.(i)) then Not_subterm
-    else 
-      let (ctxt,clfix) = dest_prod renv.env typarray.(i) in	    
+    else
+      let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
       let oind =
         let env' = push_rel_context ctxt renv.env in
           try Some(fst(find_inductive env' clfix))
@@ -767,39 +767,39 @@ let rec subterm_specif renv stack t =
         (match oind with
       None -> Not_subterm (* happens if fix is polymorphic *)
         | Some (ind, _) ->
-	let nbfix = Array.length typarray in
-	let recargs = lookup_subterms renv.env ind in
-		   (* pushing the fixpoints *)
-	let renv' = push_fix_renv renv recdef in
-	let renv' =
+        let nbfix = Array.length typarray in
+        let recargs = lookup_subterms renv.env ind in
+                   (* pushing the fixpoints *)
+        let renv' = push_fix_renv renv recdef in
+        let renv' =
                      (* Why Strict here ? To be general, it could also be
-			Large... *)
+                        Large... *)
           assign_var_spec renv'
-	  (nbfix-i, lazy (Subterm(Strict,recargs))) in
-	let decrArg = recindxs.(i) in
-	let theBody = bodies.(i)   in
-	let nbOfAbst = decrArg+1 in
-	let sign,strippedBody = Term.decompose_lam_n_assum nbOfAbst theBody in
-		   (* pushing the fix parameters *)
-	let stack' = push_stack_closures renv l stack in
-	let renv'' = push_ctxt_renv renv' sign in
-	let renv'' =
+          (nbfix-i, lazy (Subterm(Strict,recargs))) in
+        let decrArg = recindxs.(i) in
+        let theBody = bodies.(i)   in
+        let nbOfAbst = decrArg+1 in
+        let sign,strippedBody = Term.decompose_lam_n_assum nbOfAbst theBody in
+                   (* pushing the fix parameters *)
+        let stack' = push_stack_closures renv l stack in
+        let renv'' = push_ctxt_renv renv' sign in
+        let renv'' =
           if List.length stack' < nbOfAbst then renv''
           else
-	    let decrArg = List.nth stack' decrArg in
+            let decrArg = List.nth stack' decrArg in
             let arg_spec = stack_element_specif decrArg in
-	      assign_var_spec renv'' (1, arg_spec) in
-	  subterm_specif renv'' [] strippedBody)
+              assign_var_spec renv'' (1, arg_spec) in
+          subterm_specif renv'' [] strippedBody)
 
     | Lambda (x,a,b) ->
       let () = assert (List.is_empty l) in
       let spec,stack' = extract_stack stack in
-	subterm_specif (push_var renv (x,a,spec)) stack' b
+        subterm_specif (push_var renv (x,a,spec)) stack' b
 
       (* Metas and evars are considered OK *)
     | (Meta _|Evar _) -> Dead_code
 
-    | Proj (p, c) -> 
+    | Proj (p, c) ->
       let subt = subterm_specif renv stack c in
       (match subt with
        | Subterm (_s, wf) ->
@@ -850,7 +850,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) =
       (1,[],[]) renv.genv in
   raise (FixGuardError (renv.env,
                         RecursionOnIllegalTerm(fx,(arg_renv.env, arg),
-					       le_vars,lt_vars)))
+                                               le_vars,lt_vars)))
 
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
@@ -870,7 +870,7 @@ let filter_stack_domain env p stack =
       let env = push_rel_context ctx env in
       let ty, args = decompose_app (whd_all env a) in
       let elt = match kind ty with
-      | Ind ind -> 
+      | Ind ind ->
         let spec' = stack_element_specif elt in
         (match (Lazy.force spec') with
         | Not_subterm | Dead_code -> elt
@@ -894,8 +894,8 @@ let judgment_of_fixpoint (_, types, bodies) =
 let check_one_fix renv recpos trees def =
   let nfi = Array.length recpos in
 
-  (* Checks if [t] only make valid recursive calls 
-     [stack] is the list of constructor's argument specification and 
+  (* Checks if [t] only make valid recursive calls
+     [stack] is the list of constructor's argument specification and
      arguments that will be applied after reduction.
      example u in t where we have (match .. with |.. => t end) u *)
   let rec check_rec_call renv stack t =
@@ -906,24 +906,24 @@ let check_one_fix renv recpos trees def =
       match kind f with
         | Rel p ->
             (* Test if [p] is a fixpoint (recursive call) *)
-	    if renv.rel_min <= p && p < renv.rel_min+nfi then
+            if renv.rel_min <= p && p < renv.rel_min+nfi then
               begin
                 List.iter (check_rec_call renv []) l;
                 (* the position of the invoked fixpoint: *)
-	        let glob = renv.rel_min+nfi-1-p in
+                let glob = renv.rel_min+nfi-1-p in
                 (* the decreasing arg of the rec call: *)
-	        let np = recpos.(glob) in
-		let stack' = push_stack_closures renv l stack in
+                let np = recpos.(glob) in
+                let stack' = push_stack_closures renv l stack in
                 if List.length stack' <= np then error_partial_apply renv glob
                 else
-		  (* Retrieve the expected tree for the argument *)
+                  (* Retrieve the expected tree for the argument *)
                   (* Check the decreasing arg is smaller *)
                   let z = List.nth stack' np in
-	          if not (check_is_subterm (stack_element_specif z) trees.(glob)) then
+                  if not (check_is_subterm (stack_element_specif z) trees.(glob)) then
                     begin match z with
-		      |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z') 
-		      |SArg _ -> error_partial_apply renv glob
-		    end
+                      |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z')
+                      |SArg _ -> error_partial_apply renv glob
+                    end
               end
             else
               begin
@@ -935,7 +935,7 @@ let check_one_fix renv recpos trees def =
                     with FixGuardError _ ->
                       check_rec_call renv stack (Term.applist(lift p c,l))
               end
-		
+
         | Case (ci,p,c_0,lrest) ->
             begin try
               List.iter (check_rec_call renv []) (c_0::p::l);
@@ -1012,15 +1012,15 @@ let check_one_fix renv recpos trees def =
             if evaluable_constant kn renv.env then
               try List.iter (check_rec_call renv []) l
               with (FixGuardError _ ) ->
-		let value = (Term.applist(constant_value_in renv.env cu, l)) in
-	        check_rec_call renv stack value
-	    else List.iter (check_rec_call renv []) l
+                let value = (Term.applist(constant_value_in renv.env cu, l)) in
+                check_rec_call renv stack value
+            else List.iter (check_rec_call renv []) l
 
         | Lambda (x,a,b) ->
             let () = assert (List.is_empty l) in
-	    check_rec_call renv [] a ;
+            check_rec_call renv [] a ;
             let spec, stack' = extract_stack stack in
-	    check_rec_call (push_var renv (x,a,spec)) stack' b
+            check_rec_call (push_var renv (x,a,spec)) stack' b
 
         | Prod (x,a,b) ->
             let () = assert (List.is_empty l && List.is_empty stack) in
@@ -1029,9 +1029,9 @@ let check_one_fix renv recpos trees def =
 
         | CoFix (_i,(_,typarray,bodies as recdef)) ->
             List.iter (check_rec_call renv []) l;
-	    Array.iter (check_rec_call renv []) typarray;
-	    let renv' = push_fix_renv renv recdef in
-	    Array.iter (check_rec_call renv' []) bodies
+            Array.iter (check_rec_call renv []) typarray;
+            let renv' = push_fix_renv renv recdef in
+            Array.iter (check_rec_call renv' []) bodies
 
         | (Ind _ | Construct _) ->
             List.iter (check_rec_call renv []) l
@@ -1061,8 +1061,8 @@ let check_one_fix renv recpos trees def =
                   List.iter (check_rec_call renv []) l
               | LocalDef (_,c,_) ->
                   try List.iter (check_rec_call renv []) l
-                  with (FixGuardError _) -> 
-		    check_rec_call renv stack (Term.applist(c,l))
+                  with (FixGuardError _) ->
+                    check_rec_call renv stack (Term.applist(c,l))
             end
 
         | Sort _ | Int _ | Float _ ->
@@ -1079,11 +1079,11 @@ let check_one_fix renv recpos trees def =
     else
       match kind (whd_all renv.env body) with
         | Lambda (x,a,b) ->
-	    check_rec_call renv [] a;
+            check_rec_call renv [] a;
             let renv' = push_var_renv renv (x,a) in
               check_nested_fix_body illformed renv' (decr-1) recArgsDecrArg b
         | _ -> illformed ()
-	    
+
   in
   check_rec_call renv [] def
 
@@ -1107,19 +1107,19 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
     let rec check_occur env n def =
       match kind (whd_all env def) with
         | Lambda (x,a,b) ->
-	    if noccur_with_meta n nbfix a then
+            if noccur_with_meta n nbfix a then
               let env' = push_rel (LocalAssum (x,a)) env in
               if Int.equal n (k + 1) then
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) =
                   try find_inductive env a
                   with Not_found ->
-		    raise_err env i (RecursionNotOnInductiveType a) in
+                    raise_err env i (RecursionNotOnInductiveType a) in
                 let mib,_ = lookup_mind_specif env (out_punivs mind) in
                 if mib.mind_finite != Finite then
                   raise_err env i (RecursionNotOnInductiveType a);
                 (mind, (env', b))
-	      else check_occur env' (n+1) b
+              else check_occur env' (n+1) b
             else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
         | _ -> raise_err env i NotEnoughAbstractionInFixBody
     in
@@ -1155,7 +1155,7 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
       try check_one_fix renv nvect trees body
       with FixGuardError (fixenv,err) ->
         error_ill_formed_rec_body fixenv err names i
-	  (push_rec_types recdef env) (judgment_of_fixpoint recdef)
+          (push_rec_types recdef env) (judgment_of_fixpoint recdef)
     done
   else
     ()
@@ -1179,22 +1179,22 @@ let rec codomain_is_coind env c =
     | Prod (x,a,b) ->
         codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
     | _ ->
-	(try find_coinductive env b
+        (try find_coinductive env b
         with Not_found ->
-	  raise (CoFixGuardError (env, CodomainNotInductiveType b)))
+          raise (CoFixGuardError (env, CodomainNotInductiveType b)))
 
 let check_one_cofix env nbfix def deftype =
   let rec check_rec_call env alreadygrd n tree vlra  t =
     if not (noccur_with_meta n nbfix t) then
       let c,args = decompose_app (whd_all env t) in
       match kind c with
-	| Rel p when  n <= p && p < n+nbfix ->
-	    (* recursive call: must be guarded and no nested recursive
+        | Rel p when  n <= p && p < n+nbfix ->
+            (* recursive call: must be guarded and no nested recursive
                call allowed *)
             if not alreadygrd then
-	      raise (CoFixGuardError (env,UnguardedRecursiveCall t))
+              raise (CoFixGuardError (env,UnguardedRecursiveCall t))
             else if not(List.for_all (noccur_with_meta n nbfix) args) then
-	      raise (CoFixGuardError (env,NestedRecursiveOccurrences))
+              raise (CoFixGuardError (env,NestedRecursiveOccurrences))
         | Construct ((_,i as cstr_kn),_u)  ->
             let lra = vlra.(i-1) in
             let mI = inductive_of_constructor cstr_kn in
@@ -1206,59 +1206,59 @@ let check_one_cofix env nbfix def deftype =
                     if noccur_with_meta n nbfix t
                     then process_args_of_constr (lr, lrar)
                     else raise (CoFixGuardError
-		                 (env,RecCallInNonRecArgOfConstructor t))
+                                 (env,RecCallInNonRecArgOfConstructor t))
                   else begin
                       check_rec_call env true n rar (dest_subterms rar) t;
                       process_args_of_constr (lr, lrar)
-		    end
+                    end
               | [],_ -> ()
               | _ -> anomaly_ill_typed ()
             in process_args_of_constr (realargs, lra)
 
         | Lambda (x,a,b) ->
-	    let () = assert (List.is_empty args) in
+            let () = assert (List.is_empty args) in
             if noccur_with_meta n nbfix a then
               let env' = push_rel (LocalAssum (x,a)) env in
               check_rec_call env' alreadygrd (n+1) tree vlra b
             else
-	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
+              raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
 
         | CoFix (_j,(_,varit,vdefs as recdef)) ->
             if List.for_all (noccur_with_meta n nbfix) args
             then
-	      if Array.for_all (noccur_with_meta n nbfix) varit then
-		let nbfix = Array.length vdefs in
-		let env' = push_rec_types recdef env in
-		(Array.iter (check_rec_call env' alreadygrd (n+nbfix) tree vlra) vdefs;
-		 List.iter (check_rec_call env alreadygrd n tree vlra) args)
+              if Array.for_all (noccur_with_meta n nbfix) varit then
+                let nbfix = Array.length vdefs in
+                let env' = push_rec_types recdef env in
+                (Array.iter (check_rec_call env' alreadygrd (n+nbfix) tree vlra) vdefs;
+                 List.iter (check_rec_call env alreadygrd n tree vlra) args)
               else
-		raise (CoFixGuardError (env,RecCallInTypeOfDef c))
-	    else
-	      raise (CoFixGuardError (env,UnguardedRecursiveCall c))
-
-	| Case (_,p,tm,vrest) ->
-	   begin
-	     let tree = match restrict_spec env (Subterm (Strict, tree)) p with
-	     | Dead_code -> assert false
-	     | Subterm (_, tree') -> tree'
-	     | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c))
-	     in
+                raise (CoFixGuardError (env,RecCallInTypeOfDef c))
+            else
+              raise (CoFixGuardError (env,UnguardedRecursiveCall c))
+
+        | Case (_,p,tm,vrest) ->
+           begin
+             let tree = match restrict_spec env (Subterm (Strict, tree)) p with
+             | Dead_code -> assert false
+             | Subterm (_, tree') -> tree'
+             | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c))
+             in
                if (noccur_with_meta n nbfix p) then
-		 if (noccur_with_meta n nbfix tm) then
-		   if (List.for_all (noccur_with_meta n nbfix) args) then
-		     let vlra = dest_subterms tree in
-		     Array.iter (check_rec_call env alreadygrd n tree vlra) vrest
-		   else
-		     raise (CoFixGuardError (env,RecCallInCaseFun c))
-		 else
-		   raise (CoFixGuardError (env,RecCallInCaseArg c))
+                 if (noccur_with_meta n nbfix tm) then
+                   if (List.for_all (noccur_with_meta n nbfix) args) then
+                     let vlra = dest_subterms tree in
+                     Array.iter (check_rec_call env alreadygrd n tree vlra) vrest
+                   else
+                     raise (CoFixGuardError (env,RecCallInCaseFun c))
+                 else
+                   raise (CoFixGuardError (env,RecCallInCaseArg c))
                else
-		 raise (CoFixGuardError (env,RecCallInCasePred c))
-	   end
+                 raise (CoFixGuardError (env,RecCallInCasePred c))
+           end
 
-	| Meta _ -> ()
+        | Meta _ -> ()
         | Evar _ ->
-	    List.iter (check_rec_call env alreadygrd n tree vlra) args
+            List.iter (check_rec_call env alreadygrd n tree vlra) args
         | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _
           | Ind _ | Fix _ | Proj _ | Int _ | Float _ ->
            raise (CoFixGuardError (env,NotGuardedForm t)) in
@@ -1279,7 +1279,7 @@ let check_cofix env (_bodynum,(names,types,bodies as recdef)) =
       try check_one_cofix fixenv nbfix bodies.(i) types.(i)
       with CoFixGuardError (errenv,err) ->
         error_ill_formed_rec_body errenv err names i
-	  fixenv (judgment_of_fixpoint recdef)
+          fixenv (judgment_of_fixpoint recdef)
     done
   else
     ()
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index c5ea32e157..1cf34977c5 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -114,7 +114,7 @@ let debug_pr_delta resolve =
 let debug_pr_subst sub =
   let l = list_contents sub in
   let f (s1,(s2,s3)) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2 ++
-			      spc () ++ str "[" ++ str s3 ++ str "]")
+                              spc () ++ str "[" ++ str s3 ++ str "]")
   in
   str "{" ++ hov 2 (prlist_with_sep pr_comma f l) ++ str "}"
 
@@ -156,8 +156,8 @@ let mp_of_delta resolve mp =
 let find_prefix resolve mp =
   let rec sub_mp = function
     | MPdot(mp,l) as mp_sup ->
-	(try Deltamap.find_mp mp_sup resolve
-	 with Not_found -> MPdot(sub_mp mp,l))
+        (try Deltamap.find_mp mp_sup resolve
+         with Not_found -> MPdot(sub_mp mp,l))
     | p -> Deltamap.find_mp p resolve
   in
   try sub_mp mp with Not_found -> mp
@@ -207,9 +207,9 @@ let inline_of_delta inline resolver =
     | None -> []
     | Some inl_lev ->
       let extract kn hint l =
-	match hint with
-	  | Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l
-	  | _ -> l
+        match hint with
+          | Inline (lev,_) -> if lev <= inl_lev then (lev,kn)::l else l
+          | _ -> l
       in
       Deltamap.fold_kn extract resolver []
 
@@ -230,12 +230,12 @@ let subst_mp0 sub mp = (* 's like subst *)
   match mp with
     | MPfile _ | MPbound _ -> Umap.find mp sub
     | MPdot (mp1,l) as mp2 ->
-	begin
+        begin
           try Umap.find mp2 sub
-	  with Not_found ->
-	    let mp1',resolve = aux mp1 in
-	    MPdot (mp1',l),resolve
-	end
+          with Not_found ->
+            let mp1',resolve = aux mp1 in
+            MPdot (mp1',l),resolve
+        end
  in
  try Some (aux mp) with Not_found -> None
 
@@ -317,7 +317,7 @@ let subst_con sub cst =
 
 let subst_pcon sub (con,u as pcon) =
   try let con', _can = subst_con0 sub con in
-	con',u
+        con',u
   with No_subst -> pcon
 
 let subst_constant sub con =
@@ -353,71 +353,71 @@ let rec map_kn f f' c =
   let func = map_kn f f' in
     match kind c with
       | Const kn -> (try f' kn with No_subst -> c)
-      | Proj (p,t) -> 
+      | Proj (p,t) ->
           let p' = Projection.map f p in
-	  let t' = func t in
-	    if p' == p && t' == t then c
-	    else mkProj (p', t')
+          let t' = func t in
+            if p' == p && t' == t then c
+            else mkProj (p', t')
       | Ind ((kn,i),u) ->
-	  let kn' = f kn in
-	  if kn'==kn then c else mkIndU ((kn',i),u)
+          let kn' = f kn in
+          if kn'==kn then c else mkIndU ((kn',i),u)
       | Construct (((kn,i),j),u) ->
-	  let kn' = f kn in
-	  if kn'==kn then c else mkConstructU (((kn',i),j),u)
+          let kn' = f kn in
+          if kn'==kn then c else mkConstructU (((kn',i),j),u)
       | Case (ci,p,ct,l) ->
-	  let ci_ind =
+          let ci_ind =
             let (kn,i) = ci.ci_ind in
-	    let kn' = f kn in
-	    if kn'==kn then ci.ci_ind else kn',i
-	  in
-	  let p' = func p in
-	  let ct' = func ct in
+            let kn' = f kn in
+            if kn'==kn then ci.ci_ind else kn',i
+          in
+          let p' = func p in
+          let ct' = func ct in
           let l' = Array.Smart.map func l in
-	    if (ci.ci_ind==ci_ind && p'==p
-		&& l'==l && ct'==ct)then c
-	    else
-	      mkCase ({ci with ci_ind = ci_ind},
-		      p',ct', l')
+            if (ci.ci_ind==ci_ind && p'==p
+                && l'==l && ct'==ct)then c
+            else
+              mkCase ({ci with ci_ind = ci_ind},
+                      p',ct', l')
       | Cast (ct,k,t) ->
-	  let ct' = func ct in
-	  let t'= func t in
-	    if (t'==t && ct'==ct) then c
-	    else mkCast (ct', k, t')
+          let ct' = func ct in
+          let t'= func t in
+            if (t'==t && ct'==ct) then c
+            else mkCast (ct', k, t')
       | Prod (na,t,ct) ->
-	  let ct' = func ct in
-	  let t'= func t in
-	    if (t'==t && ct'==ct) then c
-	    else mkProd (na, t', ct')
+          let ct' = func ct in
+          let t'= func t in
+            if (t'==t && ct'==ct) then c
+            else mkProd (na, t', ct')
       | Lambda (na,t,ct) ->
-	  let ct' = func ct in
-	  let t'= func t in
-	    if (t'==t && ct'==ct) then c
-	    else mkLambda (na, t', ct')
+          let ct' = func ct in
+          let t'= func t in
+            if (t'==t && ct'==ct) then c
+            else mkLambda (na, t', ct')
       | LetIn (na,b,t,ct) ->
-	  let ct' = func ct in
-	  let t'= func t in
-	  let b'= func b in
-	    if (t'==t && ct'==ct && b==b') then c
-	    else mkLetIn (na, b', t', ct')
+          let ct' = func ct in
+          let t'= func t in
+          let b'= func b in
+            if (t'==t && ct'==ct && b==b') then c
+            else mkLetIn (na, b', t', ct')
       | App (ct,l) ->
-	  let ct' = func ct in
+          let ct' = func ct in
           let l' = Array.Smart.map func l in
-	    if (ct'== ct && l'==l) then c
-	    else mkApp (ct',l')
+            if (ct'== ct && l'==l) then c
+            else mkApp (ct',l')
       | Evar (e,l) ->
           let l' = Array.Smart.map func l in
-	    if (l'==l) then c
-	    else mkEvar (e,l')
+            if (l'==l) then c
+            else mkEvar (e,l')
       | Fix (ln,(lna,tl,bl)) ->
           let tl' = Array.Smart.map func tl in
           let bl' = Array.Smart.map func bl in
-	    if (bl == bl'&& tl == tl') then c
-	    else mkFix (ln,(lna,tl',bl'))
+            if (bl == bl'&& tl == tl') then c
+            else mkFix (ln,(lna,tl',bl'))
       | CoFix(ln,(lna,tl,bl)) ->
           let tl' = Array.Smart.map func tl in
           let bl' = Array.Smart.map func bl in
-	    if (bl == bl'&& tl == tl') then c
-	    else mkCoFix (ln,(lna,tl',bl'))
+            if (bl == bl'&& tl == tl') then c
+            else mkCoFix (ln,(lna,tl',bl'))
       | _ -> c
 
 let subst_mps sub c =
@@ -434,9 +434,9 @@ let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
     | _ when ModPath.equal mp mpfrom -> mpto
     | MPdot (mp1,l) ->
-	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
-	  if mp1 == mp1' then mp
-	  else MPdot (mp1',l)
+        let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
+          if mp1 == mp1' then mp
+          else MPdot (mp1',l)
     | _ -> mp
 
 let replace_mp_in_kn mpfrom mpto kn =
@@ -459,7 +459,7 @@ let subset_prefixed_by mp resolver =
     match hint with
       | Inline _ -> rslv
       | Equiv _ ->
-	if mp_in_mp mp (KerName.modpath kn) then Deltamap.add_kn kn hint rslv else rslv
+        if mp_in_mp mp (KerName.modpath kn) then Deltamap.add_kn kn hint rslv else rslv
   in
   Deltamap.fold mp_prefix kn_prefix resolver empty_delta_resolver
 
@@ -479,7 +479,7 @@ let subst_mp_delta sub mp mkey =
       let mp1 = find_prefix resolve mp' in
       let resolve1 = subset_prefixed_by mp1 resolve in
       (subst_dom_delta_resolver
-	 (map_mp mp1 mkey empty_delta_resolver) resolve1),mp1
+         (map_mp mp1 mkey empty_delta_resolver) resolve1),mp1
 
 let gen_subst_delta_resolver dom subst resolver =
   let mp_apply_subst mkey mequ rslv =
@@ -491,8 +491,8 @@ let gen_subst_delta_resolver dom subst resolver =
     let kkey' = if dom then subst_kn subst kkey else kkey in
     let hint' = match hint with
       | Equiv kequ ->
-	  (try Equiv (subst_kn_delta subst kequ)
-	   with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c))
+          (try Equiv (subst_kn_delta subst kequ)
+           with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c))
       | Inline (lev,Some t) -> Inline (lev,Some (Univ.map_univ_abstracted (subst_mps subst) t))
       | Inline (_,None) -> hint
     in
@@ -510,8 +510,8 @@ let update_delta_resolver resolver1 resolver2 =
   let kn_apply_rslv kkey hint1 rslv =
     let hint = match hint1 with
       | Equiv kequ ->
-	(try Equiv (solve_delta_kn resolver2 kequ)
-	 with Change_equiv_to_inline (lev,c) -> Inline (lev, Some c))
+        (try Equiv (solve_delta_kn resolver2 kequ)
+         with Change_equiv_to_inline (lev,c) -> Inline (lev, Some c))
       | Inline (_,Some _) -> hint1
       | Inline (_,None) ->
         (try Deltamap.find_kn kkey resolver2 with Not_found -> hint1)
@@ -539,15 +539,15 @@ let join subst1 subst2 =
   let apply_subst mpk add (mp,resolve) res =
     let mp',resolve' =
       match subst_mp0 subst2 mp with
-	| None -> mp, None
-	| Some (mp',resolve') ->  mp', Some resolve' in
+        | None -> mp, None
+        | Some (mp',resolve') ->  mp', Some resolve' in
     let resolve'' =
       match resolve' with
         | Some res ->
-	    add_delta_resolver
-	      (subst_dom_codom_delta_resolver subst2 resolve) res
-	| None ->
-	    subst_codom_delta_resolver subst2 resolve
+            add_delta_resolver
+              (subst_dom_codom_delta_resolver subst2 resolve) res
+        | None ->
+            subst_codom_delta_resolver subst2 resolve
     in
     let prefixed_subst = substition_prefixed_by mpk mp' subst2 in
     Umap.join prefixed_subst (add (mp',resolve'') res)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index ccc218771a..c1ac8b1a3e 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -174,10 +174,10 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
           let mtb_old = module_type_of_module old in
           let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in
           Univ.ContextSet.add_constraints chk_cst old.mod_constraints
-	| Algebraic (NoFunctor (MEident(mp'))) ->
-	  check_modpath_equiv env' mp1 mp';
-	  old.mod_constraints
-	| _ -> error_generative_module_expected lab
+        | Algebraic (NoFunctor (MEident(mp'))) ->
+          check_modpath_equiv env' mp1 mp';
+          old.mod_constraints
+        | _ -> error_generative_module_expected lab
       in
       let mp' = MPdot (mp,lab) in
       let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in
@@ -198,28 +198,28 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
       let mp' = MPdot (mp,lab) in
       let old = match spec with
         | SFBmodule msb -> msb
-	| _ -> error_not_a_module (Label.to_string lab)
+        | _ -> error_not_a_module (Label.to_string lab)
       in
       begin match old.mod_expr with
       | Abstract ->
         let struc = destr_nofunctor old.mod_type in
-	let struc',equiv',cst =
+        let struc',equiv',cst =
           check_with_mod env' struc (idl,mp1) mp' old.mod_delta
         in
-	let new_mb =
+        let new_mb =
           { old with
             mod_type = NoFunctor struc';
             mod_type_alg = None;
             mod_delta = equiv' }
         in
-	let new_equiv = add_delta_resolver equiv equiv' in
-	let id_subst = map_mp mp' mp' equiv' in
+        let new_equiv = add_delta_resolver equiv equiv' in
+        let id_subst = map_mp mp' mp' equiv' in
         let new_after = subst_structure id_subst after in
-	before@(lab,SFBmodule new_mb)::new_after, new_equiv, cst
+        before@(lab,SFBmodule new_mb)::new_after, new_equiv, cst
       | Algebraic (NoFunctor (MEident mp0)) ->
-	let mpnew = rebuild_mp mp0 idl in
-	check_modpath_equiv env' mpnew mp;
-	before@(lab,spec)::after, equiv, Univ.ContextSet.empty
+        let mpnew = rebuild_mp mp0 idl in
+        check_modpath_equiv env' mpnew mp;
+        before@(lab,spec)::after, equiv, Univ.ContextSet.empty
       | _ -> error_generative_module_expected lab
       end
   with
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4808ed14e4..2b141cc6a7 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -286,10 +286,10 @@ let rec add_structure mp sign resolver linkinfo env =
       Environ.add_constant_key c cb linkinfo env
     |SFBmind mib ->
       let mind = mind_of_delta_kn resolver (KerName.make mp l) in
-      let mib = 
-	if mib.mind_private != None then 
-	  { mib with mind_private = Some true }
-	else mib
+      let mib =
+        if mib.mind_private != None then
+          { mib with mind_private = Some true }
+        else mib
       in
       Environ.add_mind_key mind (mib,ref linkinfo) env
     |SFBmodule mb -> add_module mb linkinfo env (* adds components as well *)
@@ -329,7 +329,7 @@ let strengthen_const mp_from l cb resolver =
     let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
       { cb with
         const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
+        const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then mb
@@ -341,7 +341,7 @@ let rec strengthen_mod mp_from mp_to mb =
       mod_type = NoFunctor struc';
       mod_delta =
         add_mp_delta_resolver mp_from mp_to
-	  (add_delta_resolver mb.mod_delta reso) }
+          (add_delta_resolver mb.mod_delta reso) }
   |MoreFunctor _ -> mb
 
 and strengthen_sig mp_from struc mp_to reso = match struc with
@@ -374,7 +374,7 @@ let strengthen mtb mp =
       mod_type = NoFunctor struc';
       mod_delta =
         add_delta_resolver mtb.mod_delta
-	  (add_mp_delta_resolver mtb.mod_mp mp reso') }
+          (add_mp_delta_resolver mtb.mod_mp mp reso') }
   |MoreFunctor _ -> mtb
 
 let inline_delta_resolver env inl mp mbid mtb delta =
@@ -382,21 +382,21 @@ let inline_delta_resolver env inl mp mbid mtb delta =
   let rec make_inline delta = function
     | [] -> delta
     | (lev,kn)::r ->
-	let kn = replace_mp_in_kn (MPbound mbid) mp kn in
-	let con = constant_of_delta_kn delta kn in
-	try
-	  let constant = lookup_constant con env in
-	  let l = make_inline delta r in
-	  match constant.const_body with
+        let kn = replace_mp_in_kn (MPbound mbid) mp kn in
+        let con = constant_of_delta_kn delta kn in
+        try
+          let constant = lookup_constant con env in
+          let l = make_inline delta r in
+          match constant.const_body with
             | Undef _ | OpaqueDef _ | Primitive _ -> l
-	    | Def body ->
-	      let constr = Mod_subst.force_constr body in
+            | Def body ->
+              let constr = Mod_subst.force_constr body in
               let ctx = Declareops.constant_polymorphic_context constant in
               let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in
               add_inline_delta_resolver kn (lev, Some constr) l
-	with Not_found ->
-	  error_no_such_label_sub (Constant.label con)
-	    (ModPath.to_string (Constant.modpath con))
+        with Not_found ->
+          error_no_such_label_sub (Constant.label con)
+            (ModPath.to_string (Constant.modpath con))
   in
   make_inline delta constants
 
@@ -407,14 +407,14 @@ let rec strengthen_and_subst_mod mb subst mp_from mp_to =
     if mb_is_an_alias then subst_module subst do_delta_dom mb
     else
       let reso',struc' =
-	strengthen_and_subst_struct struc subst
-	  mp_from mp_to false false mb.mod_delta
+        strengthen_and_subst_struct struc subst
+          mp_from mp_to false false mb.mod_delta
       in
       { mb with
-	mod_mp = mp_to;
-	mod_expr = Algebraic (NoFunctor (MEident mp_from));
-	mod_type = NoFunctor struc';
-	mod_delta = add_mp_delta_resolver mp_to mp_from reso' }
+        mod_mp = mp_to;
+        mod_expr = Algebraic (NoFunctor (MEident mp_from));
+        mod_type = NoFunctor struc';
+        mod_delta = add_mp_delta_resolver mp_to mp_from reso' }
   |MoreFunctor _ ->
     let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
     subst_module subst do_delta_dom mb
@@ -429,55 +429,55 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
           else strengthen_const mp_from l cb' reso
         in
         let item' = if cb' == cb then item else (l, SFBconst cb') in
-	let reso',rest' =
-	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+        let reso',rest' =
+          strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
         let str' =
           if rest' == rest && item' == item then str
           else item' :: rest'
         in
-	if incl then
+        if incl then
           (* If we are performing an inclusion we need to add
              the fact that the constant mp_to.l is \Delta-equivalent
              to reso(mp_from.l) *)
           let kn_from = KerName.make mp_from l in
           let kn_to = KerName.make mp_to l in
           let old_name = kn_of_delta reso kn_from in
-	  add_kn_delta_resolver kn_to old_name reso', str'
-	else
-	  (* In this case the fact that the constant mp_to.l is
-	     \Delta-equivalent to resolver(mp_from.l) is already known
-	     because reso' contains mp_to maps to reso(mp_from) *)
-	  reso', str'
+          add_kn_delta_resolver kn_to old_name reso', str'
+        else
+          (* In this case the fact that the constant mp_to.l is
+             \Delta-equivalent to resolver(mp_from.l) is already known
+             because reso' contains mp_to maps to reso(mp_from) *)
+          reso', str'
     | (l,SFBmind mib) as item :: rest ->
         let mib' = subst_mind_body subst mib in
         let item' = if mib' == mib then item else (l, SFBmind mib') in
-	let reso',rest' =
-	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+        let reso',rest' =
+          strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
         let str' =
           if rest' == rest && item' == item then str
           else item' :: rest'
         in
-	(* Same as constant *)
-	if incl then
+        (* Same as constant *)
+        if incl then
           let kn_from = KerName.make mp_from l in
           let kn_to = KerName.make mp_to l in
-	  let old_name = kn_of_delta reso kn_from in
+          let old_name = kn_of_delta reso kn_from in
           add_kn_delta_resolver kn_to old_name reso', str'
-	else
+        else
           reso', str'
     | (l,SFBmodule mb) as item :: rest ->
-	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot (mp_to,l) in
-	let mb' = if alias then
-	  subst_module subst do_delta_dom mb
-	else
-	  strengthen_and_subst_mod mb subst mp_from' mp_to'
-	in
+        let mp_from' = MPdot (mp_from,l) in
+        let mp_to' = MPdot (mp_to,l) in
+        let mb' = if alias then
+          subst_module subst do_delta_dom mb
+        else
+          strengthen_and_subst_mod mb subst mp_from' mp_to'
+        in
         let item' = if mb' == mb then item else (l, SFBmodule mb') in
-	let reso',rest' =
-	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
+        let reso',rest' =
+          strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
         let str' =
           if rest' == rest && item' == item then str
@@ -487,27 +487,27 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
            on names, hence we add the fact that the functor can only
            be equivalent to itself. If we adopt an applicative
            semantic for functor this should be changed.*)
-	if is_functor mb'.mod_type then
+        if is_functor mb'.mod_type then
           add_mp_delta_resolver mp_to' mp_to' reso', str'
-	else
+        else
           add_delta_resolver reso' mb'.mod_delta, str'
     | (l,SFBmodtype mty) as item :: rest ->
-	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot(mp_to,l) in
-	let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
-	let mty' = subst_modtype subst'
-	  (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver)
+        let mp_from' = MPdot (mp_from,l) in
+        let mp_to' = MPdot(mp_to,l) in
+        let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
+        let mty' = subst_modtype subst'
+          (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver)
           mty
         in
         let item' = if mty' == mty then item else (l, SFBmodtype mty') in
-	let reso',rest' =
+        let reso',rest' =
           strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
         let str' =
           if rest' == rest && item' == item then str
           else item' :: rest'
         in
-	add_mp_delta_resolver mp_to' mp_to' reso', str'
+        add_mp_delta_resolver mp_to' mp_to' reso', str'
 
 
 (** Let P be a module path when we write:
@@ -525,12 +525,12 @@ let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
     let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in
     let new_resolver =
       add_mp_delta_resolver mp mp_alias
-	(subst_dom_delta_resolver subst_resolver mb.mod_delta)
+        (subst_dom_delta_resolver subst_resolver mb.mod_delta)
     in
     let subst = map_mp mb.mod_mp mp new_resolver in
     let reso',struc' =
       strengthen_and_subst_struct struc subst
-	mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
+        mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
     in
     { mb with
       mod_mp = mp;
@@ -538,7 +538,7 @@ let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with
       mod_expr = Algebraic (NoFunctor (MEident mb.mod_mp));
       mod_delta =
         if include_b then reso'
-	else add_delta_resolver new_resolver reso' }
+        else add_delta_resolver new_resolver reso' }
   |MoreFunctor _ ->
     let subst = map_mp mb.mod_mp mp empty_delta_resolver in
     subst_module subst do_delta_dom_codom mb
diff --git a/kernel/names.ml b/kernel/names.ml
index b755ff0e08..148cc352f1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -83,7 +83,7 @@ end
 module Name =
 struct
   type t = Anonymous     (** anonymous identifier *)
-	 | Name of Id.t  (** non-anonymous identifier *)
+         | Name of Id.t  (** non-anonymous identifier *)
 
   let mk_name id =
     Name id
@@ -333,7 +333,7 @@ module ModPath = struct
   module Self_Hashcons = struct
     type t = module_path
     type u = (DirPath.t -> DirPath.t) * (MBId.t -> MBId.t) *
-	(string -> string)
+        (string -> string)
     let rec hashcons (hdir,huniqid,hstr as hfuns) = function
       | MPfile dir -> MPfile (hdir dir)
       | MPbound m -> MPbound (huniqid m)
@@ -727,8 +727,8 @@ type 'a tableKey =
   | RelKey of Int.t
 
 type inv_rel_key = int (* index in the [rel_context] part of environment
-			  starting by the end, {\em inverse}
-			  of de Bruijn indice *)
+                          starting by the end, {\em inverse}
+                          of de Bruijn indice *)
 
 let eq_table_key f ik1 ik2 =
   if ik1 == ik2 then true
diff --git a/kernel/names.mli b/kernel/names.mli
index 0c92a2f2bc..d43038d2f0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -81,7 +81,7 @@ end
 module Name :
 sig
   type t = Anonymous     (** anonymous identifier *)
-	 | Name of Id.t  (** non-anonymous identifier *)
+         | Name of Id.t  (** non-anonymous identifier *)
 
   val mk_name : Id.t -> t
   (** constructor *)
@@ -534,8 +534,8 @@ type 'a tableKey =
   | RelKey of Int.t
 
 type inv_rel_key = int (** index in the [rel_context] part of environment
-			  starting by the end, {e inverse}
-			  of de Bruijn indice *)
+                          starting by the end, {e inverse}
+                          of de Bruijn indice *)
 
 val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool
 val eq_constant_key : Constant.t -> Constant.t -> bool
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 63dc49ba57..ec3f15176b 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -34,9 +34,9 @@ let eq_lname ln1 ln2 =
 
 let dummy_lname = { lname = Anonymous; luid = -1 }
 
-module LNord = 
-  struct 
-    type t = lname 
+module LNord =
+  struct
+    type t = lname
     let compare l1 l2 = l1.luid - l2.luid
   end
 module LNmap = Map.Make(LNord)
@@ -44,12 +44,12 @@ module LNset = Set.Make(LNord)
 
 let lname_ctr = ref (-1)
 
-let fresh_lname n = 
+let fresh_lname n =
   incr lname_ctr;
   { lname = n; luid = !lname_ctr }
 
 (** Global names **)
-type gname = 
+type gname =
   | Gind of string * inductive (* prefix, inductive name *)
   | Gconstant of string * Constant.t (* prefix, constant name *)
   | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *)
@@ -117,7 +117,7 @@ let fresh_gcase l =
 
 let pred_ctr = ref (-1)
 
-let fresh_gpred l = 
+let fresh_gpred l =
   incr pred_ctr;
   Gpred (l,!pred_ctr)
 
@@ -252,7 +252,7 @@ type primitive =
   | Mk_ind
   | Mk_const
   | Mk_sw
-  | Mk_fix of rec_pos * int 
+  | Mk_fix of rec_pos * int
   | Mk_cofix of int
   | Mk_rel of int
   | Mk_var of Id.t
@@ -357,10 +357,10 @@ let primitive_hash = function
   | MLnot -> 41
 
 type mllambda =
-  | MLlocal        of lname 
-  | MLglobal       of gname 
+  | MLlocal        of lname
+  | MLglobal       of gname
   | MLprimitive    of primitive
-  | MLlam          of lname array * mllambda 
+  | MLlam          of lname array * mllambda
   | MLletrec       of (lname * lname array * mllambda) array * mllambda
   | MLlet          of lname * mllambda * mllambda
   | MLapp          of mllambda * mllambda array
@@ -578,25 +578,25 @@ let fv_lam l =
   let rec aux l bind fv =
     match l with
     | MLlocal l ->
-	if LNset.mem l bind then fv else LNset.add l fv
+        if LNset.mem l bind then fv else LNset.add l fv
     | MLglobal _ | MLprimitive _  | MLint _ | MLuint _ | MLfloat _ -> fv
     | MLlam (ln,body) ->
-	let bind = Array.fold_right LNset.add ln bind in
-	aux body bind fv
+        let bind = Array.fold_right LNset.add ln bind in
+        aux body bind fv
     | MLletrec(bodies,def) ->
-	let bind = 
-	  Array.fold_right (fun (id,_,_) b -> LNset.add id b) bodies bind in
-	let fv_body (_,ln,body) fv =
-	  let bind = Array.fold_right LNset.add ln bind in
-	  aux body bind fv in
-	Array.fold_right fv_body bodies (aux def bind fv)
+        let bind =
+          Array.fold_right (fun (id,_,_) b -> LNset.add id b) bodies bind in
+        let fv_body (_,ln,body) fv =
+          let bind = Array.fold_right LNset.add ln bind in
+          aux body bind fv in
+        Array.fold_right fv_body bodies (aux def bind fv)
     | MLlet(l,def,body) ->
-	aux body (LNset.add l bind) (aux def bind fv)
+        aux body (LNset.add l bind) (aux def bind fv)
     | MLapp(f,args) ->
-	let fv_arg arg fv = aux arg bind fv in
-	Array.fold_right fv_arg args (aux f bind fv)
+        let fv_arg arg fv = aux arg bind fv in
+        Array.fold_right fv_arg args (aux f bind fv)
     | MLif(t,b1,b2) ->
-	aux t bind (aux b1 bind (aux b2 bind fv))
+        aux t bind (aux b1 bind (aux b2 bind fv))
     | MLmatch(_,a,p,bs) ->
       let fv = aux a bind (aux p bind fv) in
       let fv_bs (cargs, body) fv =
@@ -614,7 +614,7 @@ let fv_lam l =
       Array.fold_right fv_bs bs fv
     (* argument, accu branch, branches *)
     | MLconstruct (_,_,_,p) ->
-	Array.fold_right (fun a fv -> aux a bind fv) p fv
+        Array.fold_right (fun a fv -> aux a bind fv) p fv
     | MLsetref(_,l) -> aux l bind fv
     | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv)
     | MLarray arr -> Array.fold_right (fun a fv -> aux a bind fv) arr fv
@@ -624,7 +624,7 @@ let fv_lam l =
 
 
 let mkMLlam params body =
-  if Array.is_empty params then body 
+  if Array.is_empty params then body
   else
     match body with
     | MLlam (params', body) -> MLlam(Array.append params params', body)
@@ -655,10 +655,10 @@ let decompose_MLlam c =
 (*s Global declaration *)
 type global =
 (*  | Gtblname of gname * Id.t array *)
-  | Gtblnorm of gname * lname array * mllambda array 
+  | Gtblnorm of gname * lname array * mllambda array
   | Gtblfixtype of gname * lname array * mllambda array
   | Glet of gname * mllambda
-  | Gletcase of 
+  | Gletcase of
       gname * lname array * annot_sw * mllambda * mllambda * mllam_branches
   | Gopen of string
   | Gtype of inductive * (tag * int) array
@@ -720,7 +720,7 @@ let hash_global g =
     in
     combinesmall 6 (combine (ind_hash ind) (Array.fold_left hash_aux 0 arr))
   | Gcomment s -> combinesmall 7 (String.hash s)
-  
+
 let global_stack = ref ([] : global list)
 
 module HashedTypeGlobal = struct
@@ -776,27 +776,27 @@ let empty_env univ =
     env_univ = univ
   }
 
-let push_rel env id = 
+let push_rel env id =
   let local = fresh_lname id.binder_name in
-  local, { env with 
-	   env_rel = MLlocal local :: env.env_rel;
-	   env_bound = env.env_bound + 1
-	 }
+  local, { env with
+           env_rel = MLlocal local :: env.env_rel;
+           env_bound = env.env_bound + 1
+         }
 
 let push_rels env ids =
-  let lnames, env_rel = 
+  let lnames, env_rel =
     Array.fold_left (fun (names,env_rel) id ->
       let local = fresh_lname id.binder_name in
       (local::names, MLlocal local::env_rel)) ([],env.env_rel) ids in
-  Array.of_list (List.rev lnames), { env with 
-			  env_rel = env_rel;
-			  env_bound = env.env_bound + Array.length ids
-			}
+  Array.of_list (List.rev lnames), { env with
+                          env_rel = env_rel;
+                          env_bound = env.env_bound + Array.length ids
+                        }
 
 let get_rel env id i =
   if i <= env.env_bound then
     List.nth env.env_rel (i-1)
-  else 
+  else
     let i = i - env.env_bound in
     try Int.List.assoc i !(env.env_urel)
     with Not_found ->
@@ -816,19 +816,19 @@ let fresh_univ () =
 
 (*s Traduction of lambda to mllambda *)
 
-let get_prod_name codom = 
+let get_prod_name codom =
   match codom with
   | MLlam(ids,_) -> ids.(0).lname
   | _ -> assert false
 
-let get_lname (_,l) = 
+let get_lname (_,l) =
   match l with
   | MLlocal id -> id
   | _ -> invalid_arg "Nativecode.get_lname"
 
 (* Collects free variables from env in an array of local names *)
-let fv_params env = 
-  let fvn, fvr = !(env.env_named), !(env.env_urel) in 
+let fv_params env =
+  let fvn, fvr = !(env.env_named), !(env.env_urel) in
   let size = List.length fvn + List.length fvr in
   let start,params = match env.env_univ with
     | None -> 0, Array.make size dummy_lname
@@ -852,7 +852,7 @@ let fv_params env =
     params
   end
 
-let generalize_fv env body = 
+let generalize_fv env body =
   mkMLlam (fv_params env) body
 
 let empty_args = [||]
@@ -864,22 +864,22 @@ let fv_args env fvn fvr =
     | Some u -> 1, let t = Array.make (size + 1) (MLint 0) in t.(0) <- MLlocal u; t
   in
   if Array.is_empty args then empty_args
-  else 
+  else
     begin
       let fvn = ref fvn in
       let i = ref start in
       while not (List.is_empty !fvn) do
-	args.(!i) <- get_var env (fst (List.hd !fvn));
-	fvn := List.tl !fvn;
-	incr i
+        args.(!i) <- get_var env (fst (List.hd !fvn));
+        fvn := List.tl !fvn;
+        incr i
       done;
       let fvr = ref fvr in
       while not (List.is_empty !fvr) do
-	let (k,_ as kml) = List.hd !fvr in
-	let n = get_lname kml in 
-	args.(!i) <- get_rel env n.lname k;
-	fvr := List.tl !fvr;
-	incr i
+        let (k,_ as kml) = List.hd !fvr in
+        let n = get_lname kml in
+        args.(!i) <- get_rel env n.lname k;
+        fvr := List.tl !fvr;
+        incr i
       done;
       args
     end
@@ -1120,14 +1120,14 @@ let ml_of_instance instance u =
     let decl,cond,paux = extract_prim (ml_of_lam env l) t in
     compile_prim decl cond paux
   | Lcase (annot,p,a,bs) ->
-      (* let predicate_uid fv_pred = compilation of p 
-         let rec case_uid fv a_uid = 
+      (* let predicate_uid fv_pred = compilation of p
+         let rec case_uid fv a_uid =
            match a_uid with
            | Accu _ => mk_sw (predicate_uid fv_pred) (case_uid fv) a_uid
-           | Ci argsi => compilation of branches 
+           | Ci argsi => compilation of branches
          compile case = case_uid fv (compilation of a) *)
       (* Compilation of the predicate *)
-         (* Remark: if we do not want to compile the predicate we 
+         (* Remark: if we do not want to compile the predicate we
             should a least compute the fv, then store the lambda representation
             of the predicate (not the mllambda) *)
       let env_p = empty_env env.env_univ in
@@ -1159,10 +1159,10 @@ let ml_of_instance instance u =
          (* remark : the call to fv_args does not add free variables in env_c *)
       let i = push_symbol (SymbMatch annot) in
       let accu =
-	MLapp(MLprimitive Mk_sw,
-	      [| get_match_code i; MLapp (MLprimitive Cast_accu, [|la_uid|]);
-		 pred;
-		 cn_fv |]) in
+        MLapp(MLprimitive Mk_sw,
+              [| get_match_code i; MLapp (MLprimitive Cast_accu, [|la_uid|]);
+                 pred;
+                 cn_fv |]) in
 (*      let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in
       let case = generalize_fv env_c body in *)
       let cn = push_global_case cn (Array.append (fv_params env_c) [|a_uid|])
@@ -1171,26 +1171,26 @@ let ml_of_instance instance u =
       (* Final result *)
       let arg = ml_of_lam env l a in
       let force =
-	if annot.asw_finite then arg
+        if annot.asw_finite then arg
         else mkForceCofix annot.asw_prefix annot.asw_ind arg in
       mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|]
-  | Lif(t,bt,bf) -> 
+  | Lif(t,bt,bf) ->
       MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf)
   | Lfix ((rec_pos, inds, start), (ids, tt, tb)) ->
-      (* let type_f fvt = [| type fix |] 
+      (* let type_f fvt = [| type fix |]
          let norm_f1 fv f1 .. fn params1 = body1
-	 ..
+         ..
          let norm_fn fv f1 .. fn paramsn = bodyn
-         let norm fv f1 .. fn = 
-	    [|norm_f1 fv f1 .. fn; ..; norm_fn fv f1 .. fn|]
-         compile fix = 
-	   let rec f1 params1 = 
+         let norm fv f1 .. fn =
+            [|norm_f1 fv f1 .. fn; ..; norm_fn fv f1 .. fn|]
+         compile fix =
+           let rec f1 params1 =
              if is_accu rec_pos.(1) then mk_fix (type_f fvt) (norm fv) params1
-	     else norm_f1 fv f1 .. fn params1
-           and .. and fn paramsn = 
-	     if is_accu rec_pos.(n) then mk_fix (type_f fvt) (norm fv) paramsn
+             else norm_f1 fv f1 .. fn params1
+           and .. and fn paramsn =
+             if is_accu rec_pos.(n) then mk_fix (type_f fvt) (norm fv) paramsn
              else norm_fn fv f1 .. fv paramsn in
-	   start
+           start
       *)
       (* Compilation of type *)
       let env_t = empty_env env.env_univ in
@@ -1214,7 +1214,7 @@ let ml_of_instance instance u =
       in
       let ml_of_fix i body =
         let varsi, bodyi = decompose_Llam_Llet body in
-        let paramsi,letsi,envi = 
+        let paramsi,letsi,envi =
           Array.fold_left mk_lam_or_let ([],[],env_n) varsi
         in
         let paramsi,letsi =
@@ -1232,32 +1232,32 @@ let ml_of_instance instance u =
       let fv_args' = Array.map (fun id -> MLlocal id) fv_params in
       let norm_params = Array.append fv_params lf in
       let t_norm_f = Array.mapi (fun i body ->
-	push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm in
+        push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm in
       let norm = fresh_gnormtbl l in
-      let norm = push_global_norm norm fv_params 
+      let norm = push_global_norm norm fv_params
          (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in
       (* Compilation of fix *)
-      let fv_args = fv_args env fvn fvr in      
+      let fv_args = fv_args env fvn fvr in
       let lf, _env = push_rels env ids in
       let lf_args = Array.map (fun id -> MLlocal id) lf in
       let mk_norm = MLapp(MLglobal norm, fv_args) in
-      let mkrec i lname = 
-	let paramsi = t_params.(i) in
-	let reci = MLlocal (paramsi.(rec_pos.(i))) in
-	let pargsi = Array.map (fun id -> MLlocal id) paramsi in
+      let mkrec i lname =
+        let paramsi = t_params.(i) in
+        let reci = MLlocal (paramsi.(rec_pos.(i))) in
+        let pargsi = Array.map (fun id -> MLlocal id) paramsi in
         let (prefix, ind) = inds.(i) in
-	let body = 
+        let body =
           MLif(MLisaccu (prefix, ind, reci),
-	       mkMLapp 
-		 (MLapp(MLprimitive (Mk_fix(rec_pos,i)), 
-			[|mk_type; mk_norm|]))
-		 pargsi,
-	       MLapp(MLglobal t_norm_f.(i), 
-		     Array.concat [fv_args;lf_args;pargsi])) 
-	in
-	(lname, paramsi, body) in
+               mkMLapp
+                 (MLapp(MLprimitive (Mk_fix(rec_pos,i)),
+                        [|mk_type; mk_norm|]))
+                 pargsi,
+               MLapp(MLglobal t_norm_f.(i),
+                     Array.concat [fv_args;lf_args;pargsi]))
+        in
+        (lname, paramsi, body) in
       MLletrec(Array.mapi mkrec lf, lf_args.(start))
-  | Lcofix (start, (ids, tt, tb)) -> 
+  | Lcofix (start, (ids, tt, tb)) ->
       (* Compilation of type *)
       let env_t = empty_env env.env_univ in
       let ml_t = Array.map (ml_of_lam env_t l) tt in
@@ -1266,7 +1266,7 @@ let ml_of_instance instance u =
       let gft = fresh_gfixtype l in
       let gft = push_global_fixtype gft params_t ml_t in
       let mk_type = MLapp(MLglobal gft, args_t) in
-      (* Compilation of norm_i *) 
+      (* Compilation of norm_i *)
       let ndef = Array.length ids in
       let lf,env_n = push_rels (empty_env env.env_univ) ids in
       let t_params = Array.make ndef [||] in
@@ -1284,46 +1284,46 @@ let ml_of_instance instance u =
       let fv_args' = Array.map (fun id -> MLlocal id) fv_params in
       let norm_params = Array.append fv_params lf in
       let t_norm_f = Array.mapi (fun i body ->
-	push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm in
+        push_global_let (t_norm_f.(i)) (mkMLlam norm_params body)) tnorm in
       let norm = fresh_gnormtbl l in
       let norm = push_global_norm norm fv_params
         (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in
       (* Compilation of fix *)
-      let fv_args = fv_args env fvn fvr in      
+      let fv_args = fv_args env fvn fvr in
       let mk_norm = MLapp(MLglobal norm, fv_args) in
       let lnorm = fresh_lname Anonymous in
       let ltype = fresh_lname Anonymous in
       let lf, _env = push_rels env ids in
       let lf_args = Array.map (fun id -> MLlocal id) lf in
       let upd i _lname cont =
-	let paramsi = t_params.(i) in
-	let pargsi = Array.map (fun id -> MLlocal id) paramsi in
-	let uniti = fresh_lname Anonymous in
-	let body =
-	  MLlam(Array.append paramsi [|uniti|],
-		MLapp(MLglobal t_norm_f.(i),
-		      Array.concat [fv_args;lf_args;pargsi])) in
-	MLsequence(MLapp(MLprimitive Upd_cofix, [|lf_args.(i);body|]),
-		   cont) in
+        let paramsi = t_params.(i) in
+        let pargsi = Array.map (fun id -> MLlocal id) paramsi in
+        let uniti = fresh_lname Anonymous in
+        let body =
+          MLlam(Array.append paramsi [|uniti|],
+                MLapp(MLglobal t_norm_f.(i),
+                      Array.concat [fv_args;lf_args;pargsi])) in
+        MLsequence(MLapp(MLprimitive Upd_cofix, [|lf_args.(i);body|]),
+                   cont) in
       let upd = Array.fold_right_i upd lf lf_args.(start) in
       let mk_let i lname cont =
-	MLlet(lname,
-	      MLapp(MLprimitive(Mk_cofix i),[| MLlocal ltype; MLlocal lnorm|]),
-	      cont) in
-      let init = Array.fold_right_i mk_let lf upd in 
+        MLlet(lname,
+              MLapp(MLprimitive(Mk_cofix i),[| MLlocal ltype; MLlocal lnorm|]),
+              cont) in
+      let init = Array.fold_right_i mk_let lf upd in
       MLlet(lnorm, mk_norm, MLlet(ltype, mk_type, init))
-  (*    	    
-      let mkrec i lname = 
-	let paramsi = t_params.(i) in
-	let pargsi = Array.map (fun id -> MLlocal id) paramsi in
-	let uniti = fresh_lname Anonymous in
-	let body = 
-	  MLapp( MLprimitive(Mk_cofix i),
-		 [|mk_type;mk_norm; 
-		   MLlam([|uniti|],
-			 MLapp(MLglobal t_norm_f.(i),
-			       Array.concat [fv_args;lf_args;pargsi]))|]) in
-	(lname, paramsi, body) in
+  (*
+      let mkrec i lname =
+        let paramsi = t_params.(i) in
+        let pargsi = Array.map (fun id -> MLlocal id) paramsi in
+        let uniti = fresh_lname Anonymous in
+        let body =
+          MLapp( MLprimitive(Mk_cofix i),
+                 [|mk_type;mk_norm;
+                   MLlam([|uniti|],
+                         MLapp(MLglobal t_norm_f.(i),
+                               Array.concat [fv_args;lf_args;pargsi]))|]) in
+        (lname, paramsi, body) in
       MLletrec(Array.mapi mkrec lf, lf_args.(start)) *)
 
   | Lint tag -> MLapp(MLprimitive Mk_int, [|MLint tag|])
@@ -1356,11 +1356,11 @@ let mllambda_of_lambda univ auxdefs l t =
   let fv_rel = !(env.env_urel) in
   let fv_named = !(env.env_named) in
   (* build the free variables *)
-  let get_lname (_,t) = 
+  let get_lname (_,t) =
    match t with
    | MLlocal x -> x
    | _ -> assert false in
-  let params = 
+  let params =
     List.append (List.map get_lname fv_rel) (List.map get_lname fv_named) in
   if List.is_empty params then
     (!global_stack, ([],[]), ml)
@@ -1372,13 +1372,13 @@ let mllambda_of_lambda univ auxdefs l t =
 
 (** Optimization of match and fix *)
 
-let can_subst l = 
+let can_subst l =
   match l with
   | MLlocal _ | MLint _ | MLuint _ | MLglobal _ -> true
   | _ -> false
 
 let subst s l =
-  if LNmap.is_empty s then l 
+  if LNmap.is_empty s then l
   else
     let rec aux l =
       match l with
@@ -1386,16 +1386,16 @@ let subst s l =
       | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> l
       | MLlam(params,body) -> MLlam(params, aux body)
       | MLletrec(defs,body) ->
-	let arec (f,params,body) = (f,params,aux body) in
-	MLletrec(Array.map arec defs, aux body)
+        let arec (f,params,body) = (f,params,aux body) in
+        MLletrec(Array.map arec defs, aux body)
       | MLlet(id,def,body) -> MLlet(id,aux def, aux body)
       | MLapp(f,args) -> MLapp(aux f, Array.map aux args)
       | MLif(t,b1,b2) -> MLif(aux t, aux b1, aux b2)
       | MLmatch(annot,a,accu,bs) ->
-	  let auxb (cargs,body) = (cargs,aux body) in
-	  MLmatch(annot,a,aux accu, Array.map auxb bs)
+          let auxb (cargs,body) = (cargs,aux body) in
+          MLmatch(annot,a,aux accu, Array.map auxb bs)
       | MLconstruct(prefix,c,tag,args) -> MLconstruct(prefix,c,tag,Array.map aux args)
-      | MLsetref(s,l1) -> MLsetref(s,aux l1) 
+      | MLsetref(s,l1) -> MLsetref(s,aux l1)
       | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2)
       | MLarray arr -> MLarray (Array.map aux arr)
       | MLisaccu (s, ind, l) -> MLisaccu (s, ind, aux l)
@@ -1418,24 +1418,24 @@ let subst_norm params args s =
 
 let subst_case params args s =
   let len = Array.length params in
-  assert (len > 0 && 
-	  Int.equal (Array.length args) len && 
-	  let r = ref true and i = ref 0 in
-	  (* we test all arguments excepted the last *)
-	  while !i < len - 1  && !r do r := can_subst args.(!i); incr i done;
-	  !r);
+  assert (len > 0 &&
+          Int.equal (Array.length args) len &&
+          let r = ref true and i = ref 0 in
+          (* we test all arguments excepted the last *)
+          while !i < len - 1  && !r do r := can_subst args.(!i); incr i done;
+          !r);
   let s = ref s in
   for i = 0 to len - 2 do
     s := add_subst params.(i) args.(i) !s
   done;
   !s, params.(len-1), args.(len-1)
-    
+
 let empty_gdef = Int.Map.empty, Int.Map.empty
 let get_norm (gnorm, _) i = Int.Map.find i gnorm
 let get_case (_, gcase) i = Int.Map.find i gcase
 
-let all_lam n bs = 
-  let f (_, l) = 
+let all_lam n bs =
+  let f (_, l) =
     match l with
     | MLlam(params, _) -> Int.equal (Array.length params) n
     | _ -> false in
@@ -1444,68 +1444,68 @@ let all_lam n bs =
 let commutative_cut annot a accu bs args =
   let mkb (c,b) =
      match b with
-     | MLlam(params, body) -> 
+     | MLlam(params, body) ->
          (c, Array.fold_left2 (fun body x v -> MLlet(x,v,body)) body params args)
      | _ -> assert false in
   MLmatch(annot, a, mkMLapp accu args, Array.map mkb bs)
 
-let optimize gdef l =   
+let optimize gdef l =
   let rec optimize s l =
     match l with
     | MLlocal id -> (try LNmap.find id s with Not_found -> l)
     | MLglobal _ | MLprimitive _ | MLint _ | MLuint _ | MLfloat _ -> l
-    | MLlam(params,body) -> 
-	MLlam(params, optimize s body)
+    | MLlam(params,body) ->
+        MLlam(params, optimize s body)
     | MLletrec(decls,body) ->
-	let opt_rec (f,params,body) = (f,params,optimize s body ) in 
-	MLletrec(Array.map opt_rec decls, optimize s body)
+        let opt_rec (f,params,body) = (f,params,optimize s body ) in
+        MLletrec(Array.map opt_rec decls, optimize s body)
     | MLlet(id,def,body) ->
-	let def = optimize s def in
-	if can_subst def then optimize (add_subst id def s) body 
-	else MLlet(id,def,optimize s body)
+        let def = optimize s def in
+        if can_subst def then optimize (add_subst id def s) body
+        else MLlet(id,def,optimize s body)
     | MLapp(f, args) ->
-	let args = Array.map (optimize s) args in
-	begin match f with
-	| MLglobal (Gnorm (_,i)) ->
-	    (try
-	      let params,body = get_norm gdef i in
-	      let s = subst_norm params args s in
-	      optimize s body	    
-	    with Not_found -> MLapp(optimize s f, args))
-	| MLglobal (Gcase (_,i)) ->
-	    (try 
-	      let params,body = get_case gdef i in
-	      let s, id, arg = subst_case params args s in
-	      if can_subst arg then optimize (add_subst id arg s) body
-	      else MLlet(id, arg, optimize s body)
-	    with Not_found ->  MLapp(optimize s f, args))
-	| _ -> 
+        let args = Array.map (optimize s) args in
+        begin match f with
+        | MLglobal (Gnorm (_,i)) ->
+            (try
+              let params,body = get_norm gdef i in
+              let s = subst_norm params args s in
+              optimize s body
+            with Not_found -> MLapp(optimize s f, args))
+        | MLglobal (Gcase (_,i)) ->
+            (try
+              let params,body = get_case gdef i in
+              let s, id, arg = subst_case params args s in
+              if can_subst arg then optimize (add_subst id arg s) body
+              else MLlet(id, arg, optimize s body)
+            with Not_found ->  MLapp(optimize s f, args))
+        | _ ->
             let f = optimize s f in
             match f with
             | MLmatch (annot,a,accu,bs) ->
-              if all_lam (Array.length args) bs then  
-                commutative_cut annot a accu bs args 
+              if all_lam (Array.length args) bs then
+                commutative_cut annot a accu bs args
               else MLapp(f, args)
             | _ -> MLapp(f, args)
 
-	end
+        end
     | MLif(t,b1,b2) ->
        (* This optimization is critical: it applies to all fixpoints that start
        by matching on their recursive argument *)
-	let t = optimize s t in
-	let b1 = optimize s b1 in
-	let b2 = optimize s b2 in
-	begin match t, b2 with
+        let t = optimize s t in
+        let b1 = optimize s b1 in
+        let b2 = optimize s b2 in
+        begin match t, b2 with
         | MLisaccu (_, _, l1), MLmatch(annot, l2, _, bs)
-	    when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs)
+            when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs)
         | _, _ -> MLif(t, b1, b2)
-	end
+        end
     | MLmatch(annot,a,accu,bs) ->
-	let opt_b (cargs,body) = (cargs,optimize s body) in
-	MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs)
+        let opt_b (cargs,body) = (cargs,optimize s body) in
+        MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs)
     | MLconstruct(prefix,c,tag,args) ->
         MLconstruct(prefix,c,tag,Array.map (optimize s) args)
-    | MLsetref(r,l) -> MLsetref(r, optimize s l) 
+    | MLsetref(r,l) -> MLsetref(r, optimize s l)
     | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2)
     | MLarray arr -> MLarray (Array.map (optimize s) arr)
     | MLisaccu (pf, ind, l) -> MLisaccu (pf, ind, optimize s l)
@@ -1516,15 +1516,15 @@ let optimize_stk stk =
   let add_global gdef g =
     match g with
     | Glet (Gnorm (_,i), body) ->
-	let (gnorm, gcase) = gdef in
-	(Int.Map.add i (decompose_MLlam body) gnorm, gcase)
+        let (gnorm, gcase) = gdef in
+        (Int.Map.add i (decompose_MLlam body) gnorm, gcase)
     | Gletcase(Gcase (_,i), params, annot,a,accu,bs) ->
-	let (gnorm,gcase) = gdef in
-	(gnorm, Int.Map.add i (params,MLmatch(annot,a,accu,bs)) gcase)
+        let (gnorm,gcase) = gdef in
+        (gnorm, Int.Map.add i (params,MLmatch(annot,a,accu,bs)) gcase)
     | Gletcase _ -> assert false
     | _ -> gdef in
   let gdef = List.fold_left add_global empty_gdef stk in
-  let optimize_global g = 
+  let optimize_global g =
     match g with
     | Glet(Gconstant (prefix, c), body) ->
         Glet(Gconstant (prefix, c), optimize gdef body)
@@ -1596,7 +1596,7 @@ let string_of_gname g =
   | Gnorm (l,i) ->
       Format.sprintf "norm_%s_%i" (string_of_label_def l) i
   | Ginternal s -> Format.sprintf "%s" s
-  | Gnormtbl (l,i) -> 
+  | Gnormtbl (l,i) ->
       Format.sprintf "normtbl_%s_%i" (string_of_label_def l) i
   | Grel i ->
       Format.sprintf "rel_%i" i
@@ -1633,19 +1633,19 @@ let pp_mllam fmt l =
     | MLglobal g -> Format.fprintf fmt "@[%a@]" pp_gname g
     | MLprimitive p -> Format.fprintf fmt "@[%a@]" pp_primitive p
     | MLlam(ids,body) ->
-	Format.fprintf fmt "@[(fun%a@ ->@\n %a)@]"
-	  pp_ldecls ids pp_mllam body
+        Format.fprintf fmt "@[(fun%a@ ->@\n %a)@]"
+          pp_ldecls ids pp_mllam body
     | MLletrec(defs, body) ->
-	Format.fprintf fmt "@[%a@ in@\n%a@]" pp_letrec defs 
-	  pp_mllam body
+        Format.fprintf fmt "@[%a@ in@\n%a@]" pp_letrec defs
+          pp_mllam body
     | MLlet(id,def,body) ->
-	Format.fprintf fmt "@[(let@ %a@ =@\n %a@ in@\n%a)@]"
+        Format.fprintf fmt "@[(let@ %a@ =@\n %a@ in@\n%a)@]"
           pp_lname id pp_mllam def pp_mllam body
     | MLapp(f, args) ->
-	Format.fprintf fmt "@[%a@ %a@]" pp_mllam f (pp_args true) args
+        Format.fprintf fmt "@[%a@ %a@]" pp_mllam f (pp_args true) args
     | MLif(t,l1,l2) ->
-	Format.fprintf fmt "@[(if %a then@\n  %a@\nelse@\n  %a)@]"
-	  pp_mllam t pp_mllam l1 pp_mllam l2 
+        Format.fprintf fmt "@[(if %a then@\n  %a@\nelse@\n  %a)@]"
+          pp_mllam t pp_mllam l1 pp_mllam l2
     | MLmatch (annot, c, accu_br, br) ->
       let ind = annot.asw_ind in
       let prefix = annot.asw_prefix in
@@ -1655,22 +1655,22 @@ let pp_mllam fmt l =
         pp_mllam c accu pp_mllam accu_br (pp_branches prefix ind) br
 
     | MLconstruct(prefix,ind,tag,args) ->
-        Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" 
+        Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]"
           (string_of_construct prefix ~constant:false ind tag) pp_cargs args
     | MLint i -> pp_int fmt i
     | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i)
     | MLfloat f -> Format.fprintf fmt "(%s)" (Float64.compile f)
     | MLsetref (s, body) ->
-	Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body
+        Format.fprintf fmt "@[%s@ :=@\n %a@]" s pp_mllam body
     | MLsequence(l1,l2) ->
-	Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2
+        Format.fprintf fmt "@[%a;@\n%a@]" pp_mllam l1 pp_mllam l2
     | MLarray arr ->
        let len = Array.length arr in
        Format.fprintf fmt "@[[|";
        if 0 < len then begin
-	 for i = 0 to len - 2 do
+         for i = 0 to len - 2 do
            Format.fprintf fmt "%a;" pp_mllam arr.(i)
-	 done;
+         done;
          pp_mllam fmt arr.(len-1)
        end;
        Format.fprintf fmt "|]@]"
@@ -1684,8 +1684,8 @@ let pp_mllam fmt l =
     let len = Array.length defs in
     let pp_one_rec (fn, argsn, body) =
       Format.fprintf fmt "%a%a =@\n  %a"
-	pp_lname fn 
-	pp_ldecls argsn pp_mllam body in
+        pp_lname fn
+        pp_ldecls argsn pp_mllam body in
     Format.fprintf fmt "@[let rec ";
     pp_one_rec defs.(0);
     for i = 1 to len - 1 do
@@ -1697,9 +1697,9 @@ let pp_mllam fmt l =
     match l with
     | MLprimitive (Mk_prod | Mk_sort) (* FIXME: why this special case? *)
     | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
-	Format.fprintf fmt "(%a)" pp_mllam l
+        Format.fprintf fmt "(%a)" pp_mllam l
     | MLconstruct(_,_,_,args) when Array.length args > 0 ->
-	Format.fprintf fmt "(%a)" pp_mllam l
+        Format.fprintf fmt "(%a)" pp_mllam l
     | _ -> pp_mllam fmt l
 
   and pp_args sep fmt args =
@@ -1708,7 +1708,7 @@ let pp_mllam fmt l =
     if len > 0 then begin
       Format.fprintf fmt "%a" pp_blam args.(0);
       for i = 1 to len - 1 do
-	Format.fprintf fmt "%s%a" sep pp_blam args.(i)
+        Format.fprintf fmt "%s%a" sep pp_blam args.(i)
       done
     end
 
@@ -1719,7 +1719,7 @@ let pp_mllam fmt l =
     | 1 -> Format.fprintf fmt " %a" pp_blam args.(0)
     | _ -> Format.fprintf fmt "(%a)" (pp_args false) args
 
-  and pp_cparam fmt param = 
+  and pp_cparam fmt param =
     match param with
     | Some l -> pp_mllam fmt (MLlocal l)
     | None -> Format.fprintf fmt "_"
@@ -1729,13 +1729,13 @@ let pp_mllam fmt l =
     match len with
     | 0 -> ()
     | 1 -> Format.fprintf fmt " %a" pp_cparam params.(0)
-    | _ -> 
-	let aux fmt params =
-	  Format.fprintf fmt "%a" pp_cparam params.(0);
-	  for i = 1 to len - 1 do
-	    Format.fprintf fmt ",%a" pp_cparam params.(i)
-	  done in 
-	Format.fprintf fmt "(%a)" aux params
+    | _ ->
+        let aux fmt params =
+          Format.fprintf fmt "%a" pp_cparam params.(0);
+          for i = 1 to len - 1 do
+            Format.fprintf fmt ",%a" pp_cparam params.(i)
+          done in
+        Format.fprintf fmt "(%a)" aux params
 
   and pp_branches prefix ind fmt bs =
     let pp_branch (cargs,body) =
@@ -1757,19 +1757,19 @@ let pp_mllam fmt l =
     Array.iter pp_branch bs
 
   and pp_primitive fmt = function
-    | Mk_prod -> Format.fprintf fmt "mk_prod_accu" 
+    | Mk_prod -> Format.fprintf fmt "mk_prod_accu"
     | Mk_sort -> Format.fprintf fmt "mk_sort_accu"
     | Mk_ind -> Format.fprintf fmt "mk_ind_accu"
     | Mk_const -> Format.fprintf fmt "mk_constant_accu"
     | Mk_sw -> Format.fprintf fmt "mk_sw_accu"
-    | Mk_fix(rec_pos,start) -> 
-	let pp_rec_pos fmt rec_pos = 
-	  Format.fprintf fmt "@[[| %i" rec_pos.(0);
-	  for i = 1 to Array.length rec_pos - 1 do
-	    Format.fprintf fmt "; %i" rec_pos.(i) 
-	  done;
-	  Format.fprintf fmt " |]@]" in
-	Format.fprintf fmt "mk_fix_accu %a %i" pp_rec_pos rec_pos start
+    | Mk_fix(rec_pos,start) ->
+        let pp_rec_pos fmt rec_pos =
+          Format.fprintf fmt "@[[| %i" rec_pos.(0);
+          for i = 1 to Array.length rec_pos - 1 do
+            Format.fprintf fmt "; %i" rec_pos.(i)
+          done;
+          Format.fprintf fmt " |]@]" in
+        Format.fprintf fmt "mk_fix_accu %a %i" pp_rec_pos rec_pos start
     | Mk_cofix(start) -> Format.fprintf fmt "mk_cofix_accu %i" start
     | Mk_rel i -> Format.fprintf fmt "mk_rel_accu %i" i
     | Mk_var id ->
@@ -1810,7 +1810,7 @@ let pp_mllam fmt l =
                        pp_mllam (MLglobal (Gconstant (prefix,c)))
   in
   Format.fprintf fmt "@[%a@]" pp_mllam l
-  
+
 let pp_array fmt t =
   let len = Array.length t in
   Format.fprintf fmt "@[[|";
@@ -1820,14 +1820,14 @@ let pp_array fmt t =
   if len > 0 then
     Format.fprintf fmt "%a" pp_mllam t.(len - 1);
   Format.fprintf fmt "|]@]"
-  
+
 let pp_global fmt g =
   match g with
   | Glet (gn, c) ->
       let ids, c = decompose_MLlam c in
-      Format.fprintf fmt "@[let %a%a =@\n  %a@]@\n@." pp_gname gn 
-	pp_ldecls ids
-	pp_mllam c
+      Format.fprintf fmt "@[let %a%a =@\n  %a@]@\n@." pp_gname gn
+        pp_ldecls ids
+        pp_mllam c
   | Gopen s ->
       Format.fprintf fmt "@[open %s@]@." s
   | Gtype (ind, lar) ->
@@ -1850,15 +1850,15 @@ let pp_global fmt g =
     Format.fprintf fmt "@[type ind_%s =@\n%a@]@\n@." (string_of_ind ind) pp_const_sigs lar
   | Gtblfixtype (g, params, t) ->
       Format.fprintf fmt "@[let %a %a =@\n  %a@]@\n@." pp_gname g
-	pp_ldecls params pp_array t
+        pp_ldecls params pp_array t
   | Gtblnorm (g, params, t) ->
       Format.fprintf fmt "@[let %a %a =@\n  %a@]@\n@." pp_gname g
-	pp_ldecls params pp_array t 
+        pp_ldecls params pp_array t
   | Gletcase(gn,params,annot,a,accu,bs) ->
       Format.fprintf fmt "@[(* Hash = %i *)@\nlet rec %a %a =@\n  %a@]@\n@."
       (hash_global g)
-	pp_gname gn pp_ldecls params 
-	pp_mllam (MLmatch(annot,a,accu,bs))
+        pp_gname gn pp_ldecls params
+        pp_mllam (MLmatch(annot,a,accu,bs))
   | Gcomment s ->
       Format.fprintf fmt "@[(* %s *)@]@." s
 
@@ -1930,10 +1930,10 @@ let compile_constant env sigma prefix ~interactive con cb =
       in
       let l = Constant.label con in
       let auxdefs,code =
-	if no_univs then compile_with_fv env sigma None [] (Some l) code
-	else
-	  let univ = fresh_univ () in
-	  let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
+        if no_univs then compile_with_fv env sigma None [] (Some l) code
+        else
+          let univ = fresh_univ () in
+          let (auxdefs,code) = compile_with_fv env sigma (Some univ) [] (Some l) code in
           (auxdefs,mkMLlam [|univ|] code)
       in
       if !Flags.debug then Feedback.msg_debug (Pp.str "Generated mllambda code");
@@ -1942,18 +1942,18 @@ let compile_constant env sigma prefix ~interactive con cb =
       in
       if !Flags.debug then Feedback.msg_debug (Pp.str "Optimized mllambda code");
       code, name
-    | _ -> 
+    | _ ->
         let i = push_symbol (SymbConst con) in
-	let args =
-	  if no_univs then [|get_const_code i; MLarray [||]|]
-	  else [|get_const_code i|]
-	in
-	(*
-	let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const)
-	 *)
+        let args =
+          if no_univs then [|get_const_code i; MLarray [||]|]
+          else [|get_const_code i|]
+        in
+        (*
+        let t = mkMLlam [|univ|] (mkMLapp (MLprimitive Mk_const)
+         *)
         [Glet(Gconstant ("", con), mkMLapp (MLprimitive Mk_const) args)],
-	  if interactive then LinkedInteractive prefix
-	  else Linked prefix
+          if interactive then LinkedInteractive prefix
+          else Linked prefix
     end
 
 module StringOrd = struct type t = string let compare = String.compare end
@@ -1989,9 +1989,9 @@ let compile_mind mb mind stack =
     let name = Gind ("", ind) in
     let accu =
       let args =
-	if Int.equal (Univ.AUContext.size u) 0 then
-	  [|get_ind_code j; MLarray [||]|]
-	else [|get_ind_code j|]
+        if Int.equal (Univ.AUContext.size u) 0 then
+          [|get_ind_code j; MLarray [||]|]
+        else [|get_ind_code j|]
       in
       Glet(name, MLapp (MLprimitive Mk_ind, args))
     in
@@ -2079,7 +2079,7 @@ let compile_deps env sigma prefix ~interactive init t =
         | _ -> init
       in
       let code, name =
-	compile_constant env sigma prefix ~interactive c cb
+        compile_constant env sigma prefix ~interactive c cb
       in
       let comp_stack = code@comp_stack in
       let const_updates = Cmap_env.add c (nameref, name) const_updates in
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index ef610ce7e9..c3710cb0d6 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -23,41 +23,41 @@ let rec conv_val env pb lvl v1 v2 cu =
   else
     match kind_of_value v1, kind_of_value v2 with
     | Vfun f1, Vfun f2 ->
-	let v = mk_rel_accu lvl in
-	conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
+        let v = mk_rel_accu lvl in
+        conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
     | Vfun _f1, _ ->
-	conv_val env CONV lvl v1 (fun x -> v2 x) cu
+        conv_val env CONV lvl v1 (fun x -> v2 x) cu
     | _, Vfun _f2 ->
-	conv_val env CONV lvl (fun x -> v1 x) v2 cu
+        conv_val env CONV lvl (fun x -> v1 x) v2 cu
     | Vaccu k1, Vaccu k2 ->
-	conv_accu env pb lvl k1 k2 cu
-    | Vconst i1, Vconst i2 -> 
-	if Int.equal i1 i2 then cu else raise NotConvertible
+        conv_accu env pb lvl k1 k2 cu
+    | Vconst i1, Vconst i2 ->
+        if Int.equal i1 i2 then cu else raise NotConvertible
     | Vint64 i1, Vint64 i2 ->
       if Int64.equal i1 i2 then cu else raise NotConvertible
     | Vfloat64 f1, Vfloat64 f2 ->
         if Float64.(equal (of_float f1) (of_float f2)) then cu
         else raise NotConvertible
     | Vblock b1, Vblock b2 ->
-	let n1 = block_size b1 in
+        let n1 = block_size b1 in
         let n2 = block_size b2 in
-	if not (Int.equal (block_tag b1) (block_tag b2)) || not (Int.equal n1 n2) then
-	  raise NotConvertible;
-	let rec aux lvl max b1 b2 i cu =
-	  if Int.equal i max then 
-	    conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
-	  else
-	    let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
-	    aux lvl max b1 b2 (i+1) cu
-	in
-	aux lvl (n1-1) b1 b2 0 cu
+        if not (Int.equal (block_tag b1) (block_tag b2)) || not (Int.equal n1 n2) then
+          raise NotConvertible;
+        let rec aux lvl max b1 b2 i cu =
+          if Int.equal i max then
+            conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
+          else
+            let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
+            aux lvl max b1 b2 (i+1) cu
+        in
+        aux lvl (n1-1) b1 b2 0 cu
     | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Vblock _), _ -> raise NotConvertible
 
 and conv_accu env pb lvl k1 k2 cu =
   let n1 = accu_nargs k1 in
   let n2 = accu_nargs k2 in
   if not (Int.equal n1 n2) then raise NotConvertible;
-  if Int.equal n1 0 then 
+  if Int.equal n1 0 then
     conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
     let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
@@ -73,48 +73,48 @@ and conv_atom env pb lvl a1 a2 cu =
       if Evar.equal ev1 ev2 then
         Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu
       else raise NotConvertible
-    | Arel i1, Arel i2 -> 
-	if Int.equal i1 i2 then cu else raise NotConvertible
+    | Arel i1, Arel i2 ->
+        if Int.equal i1 i2 then cu else raise NotConvertible
     | Aind (ind1,u1), Aind (ind2,u2) ->
        if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
        else raise NotConvertible
     | Aconstant (c1,u1), Aconstant (c2,u2) ->
        if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
        else raise NotConvertible
-    | Asort s1, Asort s2 -> 
+    | Asort s1, Asort s2 ->
         sort_cmp_universes env pb s1 s2 cu
     | Avar id1, Avar id2 ->
-	if Id.equal id1 id2 then cu else raise NotConvertible
+        if Id.equal id1 id2 then cu else raise NotConvertible
     | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
-	if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
-	let cu = conv_accu env CONV lvl ac1 ac2 cu in
-	let tbl = a1.asw_reloc in
-	let len = Array.length tbl in
-	if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
-	else begin
-	    let cu = conv_val env CONV lvl p1 p2 cu in
-	    let max = len - 1 in
-	    let rec aux i cu =
-	      let tag,arity = tbl.(i) in
-	      let ci =
-		if Int.equal arity 0 then mk_const tag
-		else mk_block tag (mk_rels_accu lvl arity) in
-	      let bi1 = bs1 ci and bi2 = bs2 ci in
-	      if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
-	      else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
-	    aux 0 cu
-	  end
+        if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
+        let cu = conv_accu env CONV lvl ac1 ac2 cu in
+        let tbl = a1.asw_reloc in
+        let len = Array.length tbl in
+        if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
+        else begin
+            let cu = conv_val env CONV lvl p1 p2 cu in
+            let max = len - 1 in
+            let rec aux i cu =
+              let tag,arity = tbl.(i) in
+              let ci =
+                if Int.equal arity 0 then mk_const tag
+                else mk_block tag (mk_rels_accu lvl arity) in
+              let bi1 = bs1 ci and bi2 = bs2 ci in
+              if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
+              else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
+            aux 0 cu
+          end
     | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
-	if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
-	if f1 == f2 then cu
-	else conv_fix env lvl t1 f1 t2 f2 cu
+        if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
+        if f1 == f2 then cu
+        else conv_fix env lvl t1 f1 t2 f2 cu
     | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
       (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
-	if not (Int.equal s1 s2) then raise NotConvertible;
-	if f1 == f2 then cu
-	else
-	  if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
-	  else conv_fix env lvl t1 f1 t2 f2 cu 
+        if not (Int.equal s1 s2) then raise NotConvertible;
+        if f1 == f2 then cu
+        else
+          if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
+          else conv_fix env lvl t1 f1 t2 f2 cu
     | Aprod(_,d1,_c1), Aprod(_,d2,_c2) ->
        let cu = conv_val env CONV lvl d1 d2 cu in
        let v = mk_rel_accu lvl in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 7a4e62cdfe..ad71557a65 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -73,7 +73,7 @@ let mkLapp f args =
 
 let mkLlam ids body =
   if Array.is_empty ids then body
-  else 
+  else
     match body with
     | Llam(ids', body) -> Llam(Array.append ids ids', body)
     | _ -> Llam(ids, body)
@@ -99,7 +99,7 @@ let decompose_Llam_Llet lam =
 
 (*s Operators on substitution *)
 let subst_id = subs_id 0
-let lift = subs_lift 
+let lift = subs_lift
 let liftn = subs_liftn
 let cons v subst = subs_cons([|v|], subst)
 let shift subst = subs_shft (1, subst)
@@ -125,7 +125,7 @@ let map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _
   | Llazy | Lforce | Lmeta _ | Lint _ | Lfloat _ -> lam
-  | Lprod(dom,codom) -> 
+  | Lprod(dom,codom) ->
       let dom' = f n dom in
       let codom' = f n codom in
       if dom == dom' && codom == codom' then lam else Lprod(dom',codom')
@@ -189,10 +189,10 @@ let map_lam_with_binders g f n lam =
     if args == args' then lam else Levar (evk, args')
 
 (*s Lift and substitution *)
- 
+
 let rec lam_exlift el lam =
   match lam with
-  | Lrel(id,i) -> 
+  | Lrel(id,i) ->
       let i' = reloc_rel i el in
       if i == i' then lam else Lrel(id,i')
   | _ -> map_lam_with_binders el_liftn lam_exlift el lam
@@ -204,9 +204,9 @@ let lam_lift k lam =
 let lam_subst_rel lam id n subst =
   match expand_rel n subst with
   | Inl(k,v) -> lam_lift k v
-  | Inr(n',_) -> 
+  | Inr(n',_) ->
       if n == n' then lam
-      else Lrel(id, n') 
+      else Lrel(id, n')
 
 let rec lam_exsubst subst lam =
   match lam with
@@ -214,11 +214,11 @@ let rec lam_exsubst subst lam =
   | _ -> map_lam_with_binders liftn lam_exsubst subst lam
 
 let lam_subst_args subst args =
-  if is_subs_id subst then args 
+  if is_subs_id subst then args
   else Array.Smart.map (lam_exsubst subst) args
-  
+
 (** Simplification of lambda expression *)
-      
+
 (* [simplify subst lam] simplify the expression [lam_subst subst lam] *)
 (* that is :                                                          *)
 (* - Reduce [let] is the definition can be substituted i.e:           *)
@@ -227,11 +227,11 @@ let lam_subst_args subst args =
 (*    - a structured constant                                         *)
 (*    - a function                                                    *)
 (* - Transform beta redex into [let] expression                       *)
-(* - Move arguments under [let]                                       *) 
+(* - Move arguments under [let]                                       *)
 (* Invariant : Terms in [subst] are already simplified and can be     *)
 (*             substituted                                            *)
-  
-let can_subst lam = 
+
+let can_subst lam =
   match lam with
   | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Llam _
   | Lmeta _ | Levar _ -> true
@@ -247,27 +247,27 @@ let merge_if t bt bf =
   let (idsf,bodyf) = decompose_Llam bf in
   let nt = Array.length idst in
   let nf = Array.length idsf in
-  let common,idst,idsf = 
-    if Int.equal nt nf then idst, [||], [||] 
+  let common,idst,idsf =
+    if Int.equal nt nf then idst, [||], [||]
     else
       if nt < nf then idst,[||], Array.sub idsf nt (nf - nt)
       else idsf, Array.sub idst nf (nt - nf), [||] in
   Llam(common,
-       Lif(lam_lift (Array.length common) t, 
-	   mkLlam idst bodyt,
-	   mkLlam idsf bodyf))
+       Lif(lam_lift (Array.length common) t,
+           mkLlam idst bodyt,
+           mkLlam idsf bodyf))
 
 let rec simplify subst lam =
   match lam with
-  | Lrel(id,i) -> lam_subst_rel lam id i subst 
+  | Lrel(id,i) -> lam_subst_rel lam id i subst
 
   | Llet(id,def,body) ->
       let def' = simplify subst def in
       if can_subst def' then simplify (cons def' subst) body
-      else 
-	let body' = simplify (lift subst) body in
-	if def == def' && body == body' then lam
-	else Llet(id,def',body')
+      else
+        let body' = simplify (lift subst) body in
+        if def == def' && body == body' then lam
+        else Llet(id,def',body')
 
   | Lapp(f,args) ->
       begin match simplify_app subst f subst args with
@@ -280,9 +280,9 @@ let rec simplify subst lam =
       let bt' = simplify subst bt in
       let bf' = simplify subst bf in
       if can_merge_if bt' bf' then merge_if t' bt' bf'
-      else 
-	if t == t' && bt == bt' && bf == bf' then lam
-	else Lif(t',bt',bf')
+      else
+        if t == t' && bt == bt' && bf == bf' then lam
+        else Lif(t',bt',bf')
   | _ -> map_lam_with_binders liftn simplify subst lam
 
 and simplify_app substf f substa args =
@@ -290,9 +290,9 @@ and simplify_app substf f substa args =
   | Lrel(id, i) ->
       begin match lam_subst_rel f id i substf with
       | Llam(ids, body) ->
-	  reduce_lapp 
-	    subst_id (Array.to_list ids) body  
-	    substa (Array.to_list args)
+          reduce_lapp
+            subst_id (Array.to_list ids) body
+            substa (Array.to_list args)
       | f' -> mkLapp f' (simplify_args substa args)
       end
   | Llam(ids, body) ->
@@ -300,16 +300,16 @@ and simplify_app substf f substa args =
   | Llet(id, def, body) ->
       let def' = simplify substf def in
       if can_subst def' then
-	simplify_app (cons def' substf) body substa args
-      else 
-	Llet(id, def', simplify_app (lift substf) body (shift substa) args)
+        simplify_app (cons def' substf) body substa args
+      else
+        Llet(id, def', simplify_app (lift substf) body (shift substa) args)
   | Lapp(f, args') ->
-      let args = Array.append 
-	  (lam_subst_args substf args') (lam_subst_args substa args) in
+      let args = Array.append
+          (lam_subst_args substf args') (lam_subst_args substa args) in
       simplify_app substf f subst_id args
   (* TODO | Lproj -> simplify if the argument is known or a known global *)
   | _ -> mkLapp (simplify substf f) (simplify_args substa args)
-  
+
 and simplify_args subst args = Array.Smart.map (simplify subst) args
 
 and reduce_lapp substf lids body substa largs =
@@ -317,12 +317,12 @@ and reduce_lapp substf lids body substa largs =
   | id::lids, a::largs ->
       let a = simplify substa a in
       if can_subst a then
-	reduce_lapp (cons a substf) lids body substa largs
+        reduce_lapp (cons a substf) lids body substa largs
       else
-	let body = reduce_lapp (lift substf) lids body (shift substa) largs in
-	Llet(id, a, body)
+        let body = reduce_lapp (lift substf) lids body (shift substa) largs in
+        Llet(id, a, body)
   | [], [] -> simplify substf body
-  | _::_, _ -> 
+  | _::_, _ ->
       Llam(Array.of_list lids,  simplify (liftn (List.length lids) substf) body)
   | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
 
@@ -345,8 +345,8 @@ let get_value lc =
 
 let make_args start _end =
   Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
-    
-(* Translation of constructors *)	
+
+(* Translation of constructors *)
 let expand_constructor prefix ind tag nparams arity =
   let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
   let ids = Array.make (nparams + arity) anon in
@@ -405,7 +405,7 @@ let lambda_of_prim env kn op args =
 
 (*i Global environment *)
 
-let get_names decl = 
+let get_names decl =
   let decl = Array.of_list decl in
   Array.map fst decl
 
@@ -428,14 +428,14 @@ module Cache =
     let get_construct_info cache env c : constructor_info =
       try ConstrTable.find cache c
       with Not_found ->
-	let ((mind,j), i) = c in
+        let ((mind,j), i) = c in
         let oib = lookup_mind mind env in
-	let oip = oib.mind_packets.(j) in
-	let tag,arity = oip.mind_reloc_tbl.(i-1) in
-	let nparams = oib.mind_nparams in
-	let r = (tag, nparams, arity) in
+        let oip = oib.mind_packets.(j) in
+        let tag,arity = oip.mind_reloc_tbl.(i-1) in
+        let nparams = oib.mind_nparams in
+        let r = (tag, nparams, arity) in
         ConstrTable.add cache c r;
-	r
+        r
   end
 
 let is_lazy t =
@@ -618,24 +618,24 @@ and lambda_of_app cache env sigma f args =
       let args = lambda_of_args cache env sigma nparams args in
       makeblock env ind tag 0 arity args
     else makeblock env ind tag (nparams - nargs) arity empty_args
-  | _ -> 
+  | _ ->
       let f = lambda_of_constr cache env sigma f in
       let args = lambda_of_args cache env sigma 0 args in
       mkLapp f args
-	
+
 and lambda_of_args cache env sigma start args =
   let nargs = Array.length args in
   if start < nargs then
-    Array.init (nargs - start) 
+    Array.init (nargs - start)
       (fun i -> lambda_of_constr cache env sigma args.(start + i))
   else empty_args
 
 let optimize lam =
   let lam = simplify subst_id lam in
-(*  if Flags.vm_draw_opt () then 
-    (msgerrnl (str "Simplify = \n" ++ pp_lam lam);flush_all()); 
+(*  if Flags.vm_draw_opt () then
+    (msgerrnl (str "Simplify = \n" ++ pp_lam lam);flush_all());
   let lam = remove_let subst_id lam in
-  if Flags.vm_draw_opt () then 
+  if Flags.vm_draw_opt () then
     (msgerrnl (str "Remove let = \n" ++ pp_lam lam);flush_all()); *)
   lam
 
@@ -643,8 +643,8 @@ let lambda_of_constr env sigma c =
   let cache = Cache.ConstrTable.create 91 in
   let lam = lambda_of_constr cache env sigma c in
 (*  if Flags.vm_draw_opt () then begin
-    (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all()); 
-    (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all()); 
+    (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all());
+    (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all());
   end; *)
   optimize lam
 
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 1dbab6c690..7f46d4e173 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -30,29 +30,29 @@ and translate_field prefix mp env acc (l,x) =
      let con = Constant.make2 mp l in
      (if !Flags.debug then
         let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
-	Feedback.msg_debug (Pp.str msg));
+        Feedback.msg_debug (Pp.str msg));
      compile_constant_field env prefix con acc cb
   | SFBmind mb ->
      (if !Flags.debug then
-	let id = mb.mind_packets.(0).mind_typename in
-	let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
-	Feedback.msg_debug (Pp.str msg));
+        let id = mb.mind_packets.(0).mind_typename in
+        let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in
+        Feedback.msg_debug (Pp.str msg));
      compile_mind_field mp l acc mb
   | SFBmodule md ->
      let mp = md.mod_mp in
      (if !Flags.debug then
-	let msg =
-	  Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
-	in
-	Feedback.msg_debug (Pp.str msg));
+        let msg =
+          Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
+        in
+        Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env md.mod_type acc
   | SFBmodtype mdtyp ->
      let mp = mdtyp.mod_mp in
      (if !Flags.debug then
-	let msg =
-	  Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
-	in
-	Feedback.msg_debug (Pp.str msg));
+        let msg =
+          Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
+        in
+        Feedback.msg_debug (Pp.str msg));
      translate_mod prefix mp env mdtyp.mod_type acc
 
 let dump_library mp dp env mod_expr =
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index e4a8344eaf..891b4bf8f7 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -17,11 +17,11 @@ open Constr
 the native compiler *)
 
 type t = t -> t
-    
+
 type accumulator (* = t (* a block [0:code;atom;arguments] *) *)
 
 type tag = int
- 
+
 type arity = int
 
 type reloc_table = (tag * arity) array
@@ -50,7 +50,7 @@ type rec_pos = int array
 
 let eq_rec_pos = Array.equal Int.equal
 
-type atom = 
+type atom =
   | Arel of int
   | Aconstant of pconstant
   | Aind of pinductive
@@ -109,13 +109,13 @@ let mk_accu (a : atom) : t =
 let get_accu (k : accumulator) =
   (Obj.magic k : Obj.t -> accu_val) ret_accu
 
-let mk_rel_accu i = 
+let mk_rel_accu i =
   mk_accu (Arel i)
 
-let rel_tbl_size = 100 
+let rel_tbl_size = 100
 let rel_tbl = Array.init rel_tbl_size mk_rel_accu
 
-let mk_rel_accu i = 
+let mk_rel_accu i =
   if i < rel_tbl_size then rel_tbl.(i)
   else mk_rel_accu i
 
@@ -125,10 +125,10 @@ let mk_rels_accu lvl len =
 let napply (f:t) (args: t array) =
   Array.fold_left (fun f a -> f a) f args
 
-let mk_constant_accu kn u = 
+let mk_constant_accu kn u =
   mk_accu (Aconstant (kn,Univ.Instance.of_array u))
 
-let mk_ind_accu ind u = 
+let mk_ind_accu ind u =
   mk_accu (Aind (ind,Univ.Instance.of_array u))
 
 let mk_sort_accu s u =
@@ -140,10 +140,10 @@ let mk_sort_accu s u =
      let s = Sorts.sort_of_univ (Univ.subst_instance_universe u s) in
      mk_accu (Asort s)
 
-let mk_var_accu id = 
+let mk_var_accu id =
   mk_accu (Avar id)
 
-let mk_sw_accu annot c p ac = 
+let mk_sw_accu annot c p ac =
   mk_accu (Acase(annot,c,p,ac))
 
 let mk_prod_accu s dom codom =
@@ -155,7 +155,7 @@ let mk_meta_accu mv ty =
 let mk_evar_accu ev args =
   mk_accu (Aevar (ev, args))
 
-let mk_proj_accu kn c = 
+let mk_proj_accu kn c =
   mk_accu (Aproj (kn,c))
 
 let atom_of_accu (k:accumulator) =
@@ -183,8 +183,8 @@ let upd_cofix (cofix :t) (cofix_fun : t) =
   | Acofix (typ,norm,pos,_) ->
       set_atom_of_accu (Obj.magic cofix) (Acofix(typ,norm,pos,cofix_fun))
   | _ -> assert false
-  
-let force_cofix (cofix : t) = 
+
+let force_cofix (cofix : t) =
   let accu = (Obj.magic cofix : accumulator) in
   let atom = atom_of_accu accu in
   match atom with
@@ -235,7 +235,7 @@ let block_size (b:block) =
 
 let block_field (b:block) i = (Obj.magic (Obj.field (Obj.magic b) i) : t)
 
-let block_tag (b:block) = 
+let block_tag (b:block) =
   Obj.tag (Obj.magic b)
 
 type kind_of_value =
@@ -258,7 +258,7 @@ let kind_of_value (v:t) =
     else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
     else if (tag < Obj.lazy_tag) then Vblock (Obj.magic v)
       else
-        (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag); 
+        (* assert (tag = Obj.closure_tag || tag = Obj.infix_tag);
            or ??? what is 1002*)
         Vfun v
 
@@ -296,7 +296,7 @@ let no_check_add  x y =
 [@@ocaml.inline always]
 
 let add accu x y =
-  if is_int x && is_int y then no_check_add x y 
+  if is_int x && is_int y then no_check_add x y
   else accu x y
 
 let no_check_sub x y =
@@ -320,7 +320,7 @@ let no_check_div x y =
 [@@ocaml.inline always]
 
 let div accu x y =
-  if is_int x && is_int y then no_check_div x y 
+  if is_int x && is_int y then no_check_div x y
   else accu x y
 
 let no_check_rem x y =
@@ -372,12 +372,12 @@ let l_or accu x y =
   else accu x y
 
 [@@@ocaml.warning "-37"]
-type coq_carry = 
+type coq_carry =
   | Caccu of t
   | C0 of t
   | C1 of t
 
-type coq_pair = 
+type coq_pair =
   | Paccu of t
   | PPair of t * t
 
@@ -404,7 +404,7 @@ let subc accu x y =
   else accu x y
 
 let no_check_addCarryC x y =
-  let s = 
+  let s =
     Uint63.add (Uint63.add (to_uint x) (to_uint y))
       (Uint63.of_int 1) in
   mkCarry (Uint63.le s (to_uint x)) s
@@ -412,10 +412,10 @@ let no_check_addCarryC x y =
 
 let addCarryC accu x y =
   if is_int x && is_int y then no_check_addCarryC x y
-  else accu x y 
+  else accu x y
 
 let no_check_subCarryC x y =
-  let s = 
+  let s =
     Uint63.sub (Uint63.sub (to_uint x) (to_uint y))
       (Uint63.of_int 1) in
   mkCarry (Uint63.le (to_uint x) (to_uint y)) s
@@ -423,7 +423,7 @@ let no_check_subCarryC x y =
 
 let subCarryC accu x y =
   if is_int x && is_int y then no_check_subCarryC x y
-  else accu x y 
+  else accu x y
 
 let of_pair (x, y) =
   (Obj.magic (PPair(mk_uint x, mk_uint y)):t)
@@ -472,7 +472,7 @@ type coq_bool =
 
 type coq_cmp =
   | CmpAccu of t
-  | CmpEq 
+  | CmpEq
   | CmpLt
   | CmpGt
 
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 815ef3e98e..420249117d 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -36,7 +36,7 @@ val eq_annot_sw : annot_sw -> annot_sw -> bool
 val hash_annot_sw : annot_sw -> int
 
 type sort_annot = string * int
-      
+
 type rec_pos = int array
 
 val eq_rec_pos : rec_pos -> rec_pos -> bool
@@ -47,8 +47,8 @@ type atom =
   | Aind of pinductive
   | Asort of Sorts.t
   | Avar of Id.t
-  | Acase of annot_sw * accumulator * t * (t -> t) 
-  | Afix of t array * t array * rec_pos * int 
+  | Acase of annot_sw * accumulator * t * (t -> t)
+  | Afix of t array * t array * rec_pos * int
   | Acofix of t array * t array * int * t
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
@@ -89,7 +89,7 @@ val mk_meta_accu : metavariable -> t
 val mk_evar_accu : Evar.t -> t array -> t
 val mk_proj_accu : (inductive * int) -> accumulator -> t
 val upd_cofix : t -> t -> unit
-val force_cofix : t -> t 
+val force_cofix : t -> t
 val mk_const : tag -> t
 val mk_block : tag -> t array -> t
 
@@ -117,9 +117,9 @@ val cast_accu : t -> accumulator
 [@@ocaml.inline always]
 
 (* Functions over block: i.e constructors *)
-    
+
 type block
-      
+
 val block_size : block -> int
 val block_field : block -> int -> t
 val block_tag : block -> int
@@ -178,7 +178,7 @@ val addMulDiv : t -> t -> t -> t -> t
 val eq      : t -> t -> t -> t
 val lt      : t -> t -> t -> t
 val le      : t -> t -> t -> t
-val compare : t -> t -> t -> t 
+val compare : t -> t -> t -> t
 
 val print : t -> t
 
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f0b706e4f5..774bdc92fb 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -13,7 +13,7 @@ open Univ
 open Constr
 open Mod_subst
 
-type work_list = (Instance.t * Id.t array) Cmap.t * 
+type work_list = (Instance.t * Id.t array) Cmap.t *
   (Instance.t * Id.t array) Mindmap.t
 
 type cooking_info = {
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0cc7692fcf..f2cb9a8aec 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -209,7 +209,7 @@ type conv_pb =
 
 let is_cumul = function CUMUL -> true | CONV -> false
 
-type 'a universe_compare = 
+type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
@@ -281,9 +281,9 @@ let conv_table_key infos k1 k2 cuniv =
   match k1, k2 with
   | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' ->
     if Univ.Instance.equal u u' then cuniv
-    else 
-      let flex = evaluable_constant cst (info_env infos) 
-	&& RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
+    else
+      let flex = evaluable_constant cst (info_env infos)
+        && RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
       in convert_instances ~flex u u' cuniv
   | VarKey id, VarKey id' when Id.equal id id' -> cuniv
   | RelKey n, RelKey n' when Int.equal n n' -> cuniv
@@ -351,16 +351,16 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   match (fterm_of hd1, fterm_of hd2) with
     (* case of leaves *)
     | (FAtom a1, FAtom a2) ->
-	(match kind a1, kind a2 with
-	   | (Sort s1, Sort s2) ->
-	       if not (is_empty_stack v1 && is_empty_stack v2) then
-		 anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
+        (match kind a1, kind a2 with
+           | (Sort s1, Sort s2) ->
+               if not (is_empty_stack v1 && is_empty_stack v2) then
+                 anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
               sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv
-	   | (Meta n, Meta m) ->
+           | (Meta n, Meta m) ->
                if Int.equal n m
                then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
                else raise NotConvertible
-	   | _ -> raise NotConvertible)
+           | _ -> raise NotConvertible)
     | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
         if Evar.equal ev1 ev2 then
           let el1 = el_stack lft1 v1 in
@@ -405,8 +405,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     | (FProj (p1,c1), FProj (p2, c2)) ->
       (* Projections: prefer unfolding to first-order unification,
-	 which will happen naturally if the terms c1, c2 are not in constructor
-	 form *)
+         which will happen naturally if the terms c1, c2 are not in constructor
+         form *)
       (match unfold_projection infos.cnv_inf p1 with
       | Some s1 ->
         eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
@@ -422,7 +422,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
             let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
               convert_stacks l2r infos lft1 lft2 v1 v2 u1
           else (* Two projections in WHNF: unfold *)
-	    raise NotConvertible)
+            raise NotConvertible)
 
     | (FProj (p1,c1), t2) ->
       begin match unfold_projection infos.cnv_inf p1 with
@@ -471,8 +471,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     | (FProd (x1, c1, c2, e), FProd (_, c'1, c'2, e')) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
-	  anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
-	(* Luo's system *)
+          anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
+        (* Luo's system *)
         let el1 = el_stack lft1 v1 in
         let el2 = el_stack lft2 v2 in
         let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
@@ -493,8 +493,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         let () = match v2 with
         | [] -> ()
         | _ ->
-	  anomaly (Pp.str "conversion was given unreduced term (FLambda).")
-	in
+          anomaly (Pp.str "conversion was given unreduced term (FLambda).")
+        in
         let (x2,_ty2,bd2) = destFLambda mk_clos hd2 in
         let infos = push_relevance infos x2 in
         eqappr CONV l2r infos
@@ -569,26 +569,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
             let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
             convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
-	  
+
     (* Eta expansion of records *)
     | (FConstruct ((ind1,_j1),_u1), _) ->
       (try
-    	 let v1, v2 =
+         let v1, v2 =
             eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
          in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (_, FConstruct ((ind2,_j2),_u2)) ->
       (try
-    	 let v2, v1 =
+         let v2, v1 =
             eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
          in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (FFix (((op1, i1),(na1,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
         if Int.equal i1 i2 && Array.equal Int.equal op1 op2
-	then
-	  let n = Array.length cl1 in
+        then
+          let n = Array.length cl1 in
           let fty1 = Array.map (mk_clos e1) tys1 in
           let fty2 = Array.map (mk_clos e2) tys2 in
           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
@@ -607,7 +607,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FCoFix ((op1,(na1,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
         if Int.equal op1 op2
         then
-	  let n = Array.length cl1 in
+          let n = Array.length cl1 in
           let fty1 = Array.map (mk_clos e1) tys1 in
           let fty2 = Array.map (mk_clos e2) tys2 in
           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
@@ -712,10 +712,10 @@ let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
 
-let check_eq univs u u' = 
+let check_eq univs u u' =
   if not (UGraph.check_eq univs u u') then raise NotConvertible
 
-let check_leq univs u u' = 
+let check_leq univs u u' =
   if not (UGraph.check_leq univs u u') then raise NotConvertible
 
 let check_sort_cmp_universes env pb s0 s1 univs =
@@ -787,7 +787,7 @@ let infer_cmp_universes env pb s0 s1 univs =
 
 let infer_convert_instances ~flex u u' (univs,cstrs) =
   let cstrs' =
-    if flex then 
+    if flex then
       if UGraph.check_eq_instances univs u u' then cstrs
       else raise NotConvertible
     else Univ.enforce_eq_instances u u' cstrs
@@ -803,14 +803,14 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
     compare_cumul_instances = infer_inductive_instances; }
 
 let gen_conv cv_pb l2r reds env evars univs t1 t2 =
-  let b = 
-    if cv_pb = CUMUL then leq_constr_univs univs t1 t2 
+  let b =
+    if cv_pb = CUMUL then leq_constr_univs univs t1 t2
     else eq_constr_univs univs t1 t2
   in
     if b then ()
-    else 
+    else
       let _ = clos_gen_conv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in
-	()
+        ()
 
 (* Profiling *)
 let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None), universes env) =
@@ -825,8 +825,8 @@ let conv = gen_conv CONV
 let conv_leq = gen_conv CUMUL
 
 let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
-  let (s, _) = 
-    clos_gen_conv reds cv_pb l2r evars env univs t1 t2 
+  let (s, _) =
+    clos_gen_conv reds cv_pb l2r evars env univs t1 t2
   in s
 
 let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
@@ -838,21 +838,21 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
     else
       let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
       let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs t1 t2 in
-	cstrs
+        cstrs
 
 (* Profiling *)
-let infer_conv_universes = 
-  if Flags.profile then 
+let infer_conv_universes =
+  if Flags.profile then
     let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
       CProfile.profile8 infer_conv_universes_key infer_conv_universes
   else infer_conv_universes
 
 let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
-    env univs t1 t2 = 
+    env univs t1 t2 =
   infer_conv_universes CONV l2r evars ts env univs t1 t2
 
 let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
-    env univs t1 t2 = 
+    env univs t1 t2 =
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
 let default_conv cv_pb ?l2r:_ env t1 t2 =
@@ -923,7 +923,7 @@ let dest_prod env =
     match kind t with
       | Prod (n,a,c0) ->
           let d = LocalAssum (n,a) in
-	  decrec (push_rel d env) (Context.Rel.add d m) c0
+          decrec (push_rel d env) (Context.Rel.add d m) c0
       | _ -> m,t
   in
   decrec env Context.Rel.empty
@@ -946,14 +946,14 @@ let dest_prod_assum env =
     match kind rty with
     | Prod (x,t,c)  ->
         let d = LocalAssum (x,t) in
-	prodec_rec (push_rel d env) (Context.Rel.add d l) c
+        prodec_rec (push_rel d env) (Context.Rel.add d l) c
     | LetIn (x,b,t,c) ->
         let d = LocalDef (x,b,t) in
-	prodec_rec (push_rel d env) (Context.Rel.add d l) c
+        prodec_rec (push_rel d env) (Context.Rel.add d l) c
     | _               ->
       let rty' = whd_all env rty in
-	if Constr.equal rty' rty then l, rty
-	else prodec_rec env l rty'
+        if Constr.equal rty' rty then l, rty
+        else prodec_rec env l rty'
   in
   prodec_rec env Context.Rel.empty
 
@@ -963,10 +963,10 @@ let dest_lam_assum env =
     match kind rty with
     | Lambda (x,t,c)  ->
         let d = LocalAssum (x,t) in
-	lamec_rec (push_rel d env) (Context.Rel.add d l) c
+        lamec_rec (push_rel d env) (Context.Rel.add d l) c
     | LetIn (x,b,t,c) ->
         let d = LocalDef (x,b,t) in
-	lamec_rec (push_rel d env) (Context.Rel.add d l) c
+        lamec_rec (push_rel d env) (Context.Rel.add d l) c
     | _               -> l,rty
   in
   lamec_rec env Context.Rel.empty
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ab34d3a6dc..ecd6b89388 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -29,7 +29,7 @@ val nf_betaiota      : env -> constr -> constr
 exception NotConvertible
 
 type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
-type 'a extended_conversion_function = 
+type 'a extended_conversion_function =
   ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:((existential->constr option) * UGraph.t) ->
   'a -> 'a -> unit
@@ -75,9 +75,9 @@ val conv_leq : types extended_conversion_function
 
 (** These conversion functions are used by module subtyping, which needs to infer
     universe constraints inside the kernel *)
-val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> 
+val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) ->
   ?ts:TransparentState.t -> constr infer_conversion_function
-val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
+val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) ->
   ?ts:TransparentState.t -> types infer_conversion_function
 
 (** Depending on the universe state functions, this might raise
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d3cffd1546..06f5aae047 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -341,7 +341,7 @@ let push_context_set poly cst senv =
 
 let add_constraints cst senv =
   match cst with
-  | Later fc -> 
+  | Later fc ->
     {senv with future_cst = fc :: senv.future_cst}
   | Now cst ->
     push_context_set false cst senv
@@ -360,7 +360,7 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e =
        else add_constraints (Now (Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
-let is_joined_environment e = List.is_empty e.future_cst 
+let is_joined_environment e = List.is_empty e.future_cst
 
 (** {6 Various checks } *)
 
@@ -493,7 +493,7 @@ let globalize_constant_universes cb =
     [cstrs]
   | Polymorphic _ ->
     []
-      
+
 let globalize_mind_universes mb =
   match mb.mind_universes with
   | Monomorphic ctx ->
@@ -1185,11 +1185,11 @@ let add_include me is_module inl senv =
     | MoreFunctor(mbid,mtb,str) ->
       let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
       let senv =
-	add_constraints
+        add_constraints
           (Now (Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty))
-	  senv in
+          senv in
       let mpsup_delta =
-	Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
+        Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
       in
       let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in
       let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in
@@ -1291,8 +1291,8 @@ let import lib cst vodigest senv =
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
   let env = Environ.push_context_set ~strict:true
-				     (Univ.ContextSet.union mb.mod_constraints cst)
-				     senv.env
+                                     (Univ.ContextSet.union mb.mod_constraints cst)
+                                     senv.env
   in
   let env =
     let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index b8bebb659b..01ee91d108 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -111,9 +111,9 @@ module Hsorts =
       type u = Universe.t -> Universe.t
 
       let hashcons huniv = function
-        | Type u as c -> 
-	  let u' = huniv u in 
-	    if u' == u then c else Type u'
+        | Type u as c ->
+          let u' = huniv u in
+            if u' == u then c else Type u'
         | s -> s
       let eq s1 s2 = match (s1,s2) with
         | Prop, Prop | Set, Set -> true
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d22ec3b7ca..0a654adf7f 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -84,11 +84,11 @@ let make_labmap mp list =
 
 
 let check_conv_error error why cst poly f env a1 a2 =
-  try 
+  try
     let cst' = f env (Environ.universes env) a1 a2 in
-      if poly then 
-	if Constraint.is_empty cst' then cst
-	else error (IncompatiblePolymorphism (env, a1, a2))
+      if poly then
+        if Constraint.is_empty cst' then cst
+        else error (IncompatiblePolymorphism (env, a1, a2))
       else Constraint.union cst cst'
   with NotConvertible -> error why
      | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
@@ -116,7 +116,7 @@ let check_variance error v1 v2 =
 
 (* for now we do not allow reorderings *)
 
-let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
+let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2=
   let kn1 = KerName.make mp1 l in
   let kn2 = KerName.make mp2 l in
   let error why = error_signature_mismatch l spec2 why in
@@ -153,7 +153,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       let ty1 = type_of_inductive env ((mib1, p1), inst) in
       let ty2 = type_of_inductive env ((mib2, p2), inst) in
       let cst = check_inductive_type cst p2.mind_typename ty1 ty2 in
-	cst
+        cst
   in
   let mind = MutInd.make1 kn1 in
   let check_cons_types _i cst p1 p2 =
@@ -170,7 +170,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x);
   assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps);
   assert (Array.length mib1.mind_packets >= 1
-	    && Array.length mib2.mind_packets >= 1);
+            && Array.length mib2.mind_packets >= 1);
 
   (* Check that the expected numbers of uniform parameters are the same *)
   (* No need to check the contexts of parameters: it is checked *)
@@ -217,7 +217,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   in
     cst
 
-    
+
 let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
   let error why = error_signature_mismatch l spec2 why in
   let check_conv cst poly f = check_conv_error error cst poly f in
@@ -238,21 +238,21 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
       let typ2 = cb2.const_type in
       let cst = check_type poly cst env typ1 typ2 in
       (* Now we check the bodies:
-	 - A transparent constant can only be implemented by a compatible
-	   transparent constant.
+         - A transparent constant can only be implemented by a compatible
+           transparent constant.
          - In the signature, an opaque is handled just as a parameter:
            anything of the right type can implement it, even if bodies differ.
       *)
       (match cb2.const_body with
         | Primitive _ | Undef _ | OpaqueDef _ -> cst
-	| Def lc2 ->
-	  (match cb1.const_body with
+        | Def lc2 ->
+          (match cb1.const_body with
             | Primitive _ | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField
-	    | Def lc1 ->
-	      (* NB: cb1 might have been strengthened and appear as transparent.
-		 Anyway [check_conv] will handle that afterwards. *)
-	      let c1 = Mod_subst.force_constr lc1 in
-	      let c2 = Mod_subst.force_constr lc2 in
+            | Def lc1 ->
+              (* NB: cb1 might have been strengthened and appear as transparent.
+                 Anyway [check_conv] will handle that afterwards. *)
+              let c1 = Mod_subst.force_constr lc1 in
+              let c2 = Mod_subst.force_constr lc2 in
               check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2))
    | IndType ((_kn,_i),_mind1) ->
        CErrors.user_err Pp.(str @@
@@ -272,31 +272,31 @@ let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty2 =  module_type_of_module msb2 in
   check_modtypes cst env mty1 mty2 subst1 subst2 false
 
-and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= 
+and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
   let map1 = make_labmap mp1 sig1 in
   let check_one_body cst (l,spec2) =
     match spec2 with
-	| SFBconst cb2 ->
+        | SFBconst cb2 ->
             check_constant cst env l (get_obj mp1 map1 l)
-	      cb2 spec2 subst1 subst2
-	| SFBmind mib2 ->
-	    check_inductive cst env mp1 l (get_obj mp1 map1 l)
-	      mp2 mib2 spec2 subst1 subst2 reso1 reso2
-	| SFBmodule msb2 ->
-	    begin match get_mod mp1 map1 l with
-	      | Module msb -> check_modules cst env msb msb2 subst1 subst2
-	      | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
-	    end
-	| SFBmodtype mtb2 ->
-	    let mtb1 = match get_mod mp1 map1 l with
-	      | Modtype mtb -> mtb
-	      | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
-	    in
-	    let env =
+              cb2 spec2 subst1 subst2
+        | SFBmind mib2 ->
+            check_inductive cst env mp1 l (get_obj mp1 map1 l)
+              mp2 mib2 spec2 subst1 subst2 reso1 reso2
+        | SFBmodule msb2 ->
+            begin match get_mod mp1 map1 l with
+              | Module msb -> check_modules cst env msb msb2 subst1 subst2
+              | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
+            end
+        | SFBmodtype mtb2 ->
+            let mtb1 = match get_mod mp1 map1 l with
+              | Modtype mtb -> mtb
+              | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
+            in
+            let env =
               add_module_type mtb2.mod_mp mtb2
-	        (add_module_type mtb1.mod_mp mtb1 env)
+                (add_module_type mtb1.mod_mp mtb1 env)
             in
-	    check_modtypes cst env mtb1 mtb2 subst1 subst2 true
+            check_modtypes cst env mtb1 mtb2 subst1 subst2 true
   in
     List.fold_left check_one_body cst sig2
 
@@ -307,40 +307,40 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
       match str1,str2 with
       |NoFunctor list1,
        NoFunctor list2 ->
-	if equiv then
-	  let subst2 = add_mp mtb2.mod_mp mtb1.mod_mp mtb1.mod_delta subst2 in
+        if equiv then
+          let subst2 = add_mp mtb2.mod_mp mtb1.mod_mp mtb1.mod_delta subst2 in
           let cst1 = check_signatures cst env
-	    mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2
-	    mtb1.mod_delta mtb2.mod_delta
+            mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2
+            mtb1.mod_delta mtb2.mod_delta
           in
           let cst2 = check_signatures cst env
-	    mtb2.mod_mp list2 mtb1.mod_mp list1 subst2 subst1
-	    mtb2.mod_delta  mtb1.mod_delta
-	  in
-	  Univ.Constraint.union cst1 cst2
-	else
-	  check_signatures cst env
-	    mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2
-	    mtb1.mod_delta  mtb2.mod_delta
+            mtb2.mod_mp list2 mtb1.mod_mp list1 subst2 subst1
+            mtb2.mod_delta  mtb1.mod_delta
+          in
+          Univ.Constraint.union cst1 cst2
+        else
+          check_signatures cst env
+            mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2
+            mtb1.mod_delta  mtb2.mod_delta
       |MoreFunctor (arg_id1,arg_t1,body_t1),
        MoreFunctor (arg_id2,arg_t2,body_t2) ->
         let mp2 = MPbound arg_id2 in
-	let subst1 = join (map_mbid arg_id1 mp2 arg_t2.mod_delta) subst1 in
-	let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in
+        let subst1 = join (map_mbid arg_id1 mp2 arg_t2.mod_delta) subst1 in
+        let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in
         (* contravariant *)
-	let env = add_module_type mp2 arg_t2 env in
-	let env =
+        let env = add_module_type mp2 arg_t2 env in
+        let env =
           if Modops.is_functor body_t1 then env
           else add_module
             {mod_mp = mtb1.mod_mp;
-	     mod_expr = Abstract;
-	     mod_type = subst_signature subst1 body_t1;
-	     mod_type_alg = None;
-	     mod_constraints = mtb1.mod_constraints;
-	     mod_retroknowledge = ModBodyRK [];
-	     mod_delta = mtb1.mod_delta} env
-	in
-	check_structure cst env body_t1 body_t2 equiv subst1 subst2
+             mod_expr = Abstract;
+             mod_type = subst_signature subst1 body_t1;
+             mod_type_alg = None;
+             mod_constraints = mtb1.mod_constraints;
+             mod_retroknowledge = ModBodyRK [];
+             mod_delta = mtb1.mod_delta} env
+        in
+        check_structure cst env body_t1 body_t2 equiv subst1 subst2
       | _ , _ -> error_incompatible_modtypes mtb1 mtb2
     in
     check_structure cst env mtb1.mod_type mtb2.mod_type equiv subst1 subst2
diff --git a/kernel/term.ml b/kernel/term.ml
index 7343507838..87678b911e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -380,7 +380,7 @@ let kind_of_type t = match kind t with
   | Prod (na,t,c) -> ProdType (na, t, c)
   | LetIn (na,b,t,c) -> LetInType (na, b, t, c)
   | App (c,l) -> AtomicType (c, l)
-  | (Rel _ | Meta _ | Var _ | Evar _ | Const _ 
+  | (Rel _ | Meta _ | Var _ | Evar _ | Const _
   | Proj _ | Case _ | Fix _ | CoFix _ | Ind _)
     -> AtomicType (t,[||])
   | (Lambda _ | Construct _ | Int _ | Float _) -> failwith "Not a type"
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f85b3db413..faa601e277 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -138,7 +138,7 @@ let infer_declaration env (dcl : constant_entry) =
       in
       let def = Vars.subst_univs_level_constr usubst j.uj_val in
       let def = Def (Mod_subst.from_val def) in
-	feedback_completion_typecheck feedback_id;
+        feedback_completion_typecheck feedback_id;
       {
         Cooking.cook_body = def;
         cook_type = typ;
@@ -243,7 +243,7 @@ let build_constant_declaration env result =
   in
   let univs = result.cook_universes in
   let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
-  let tps = 
+  let tps =
     let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
     Option.map Cemitcodes.from_val res
   in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1cc40a6707..c74bfd0688 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -39,7 +39,7 @@ let conv_leq_vecti env v1 v2 =
     v1
     v2
 
-let check_constraints cst env = 
+let check_constraints cst env =
   if Environ.check_constraints cst env then ()
   else error_unsatisfied_constraints env cst
 
@@ -173,7 +173,7 @@ let type_of_abstraction _env name var ty =
 
 (* Type of an application. *)
 
-let make_judgev c t = 
+let make_judgev c t =
   Array.map2 make_judge c t
 
 let rec check_empty_stack = function
@@ -371,7 +371,7 @@ let check_cast env c ct k expected_type =
 let type_of_inductive_knowing_parameters env (ind,u as indu) args =
   let (mib,_mip) as spec = lookup_mind_specif env ind in
   check_hyps_inclusion env mkIndU indu mib.mind_hyps;
-  let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters 
+  let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters
     env (spec,u) args
   in
   check_constraints cst env;
@@ -432,7 +432,7 @@ let type_of_projection env p c ct =
   assert(eq_ind (Projection.inductive p) ind);
   let ty = Vars.subst_instance_constr u pty in
   substl (c :: CList.rev args) ty
-      
+
 
 (* Fixpoints. *)
 
@@ -503,7 +503,7 @@ let rec execute env cstr =
 
     | Const c ->
       cstr, type_of_constant env c
-	
+
     | Proj (p, c) ->
       let c', ct = execute env c in
       let cstr = if c == c' then cstr else mkProj (p,c') in
@@ -513,14 +513,14 @@ let rec execute env cstr =
     | App (f,args) ->
       let args', argst = execute_array env args in
         let f', ft =
-	  match kind f with
-	  | Ind ind when Environ.template_polymorphic_pind ind env ->
-	    let args = Array.map (fun t -> lazy t) argst in
+          match kind f with
+          | Ind ind when Environ.template_polymorphic_pind ind env ->
+            let args = Array.map (fun t -> lazy t) argst in
               f, type_of_inductive_knowing_parameters env ind args
-	  | _ ->
-	    (* No template polymorphism *)
+          | _ ->
+            (* No template polymorphism *)
             execute env f
-	in
+        in
         let cstr = if f == f' && args == args' then cstr else mkApp (f',args') in
         cstr, type_of_apply env f' ft args' argst
 
@@ -582,7 +582,7 @@ let rec execute env cstr =
           let fix = (vni,recdef') in mkFix fix, fix
       in
       check_fix env fix; cstr, fix_ty
-	  
+
     | CoFix (i,recdef as cofix) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let cstr, cofix = if recdef == recdef' then cstr, cofix else
@@ -596,10 +596,10 @@ let rec execute env cstr =
 
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
-	anomaly (Pp.str "the kernel does not support metavariables.")
+        anomaly (Pp.str "the kernel does not support metavariables.")
 
     | Evar _ ->
-	anomaly (Pp.str "the kernel does not support existential variables.")
+        anomaly (Pp.str "the kernel does not support existential variables.")
 
 and execute_is_type env constr =
   let c, t = execute env constr in
@@ -632,7 +632,7 @@ let infer env constr =
   let constr, t = execute env constr in
   make_judge constr t
 
-let infer = 
+let infer =
   if Flags.profile then
     let infer_key = CProfile.declare_profile "Fast_infer" in
       CProfile.profile2 infer_key (fun b c -> infer b c)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 14d6bfabf1..0029ff96d5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -133,11 +133,11 @@ module Level = struct
   | Var of int
 
   (** Embed levels with their hash value *)
-  type t = { 
+  type t = {
     hash : int;
     data : RawLevel.t }
 
-  let equal x y = 
+  let equal x y =
     x == y || Int.equal x.hash y.hash && RawLevel.equal x.data y.data
 
   let hash x = x.hash
@@ -166,14 +166,14 @@ module Level = struct
   let prop = make Prop
   let sprop = make SProp
 
-  let is_small x = 
+  let is_small x =
     match data x with
     | Level _ -> false
     | Var _ -> false
     | SProp -> true
     | Prop -> true
     | Set -> true
- 
+
   let is_prop x =
     match data x with
     | Prop -> true
@@ -192,8 +192,8 @@ module Level = struct
   let compare u v =
     if u == v then 0
     else RawLevel.compare (data u) (data v)
-	    
-  let to_string x = 
+
+  let to_string x =
     match data x with
     | SProp -> "SProp"
     | Prop -> "Prop"
@@ -211,7 +211,7 @@ module Level = struct
 
   let vars = Array.init 20 (fun i -> make (Var i))
 
-  let var n = 
+  let var n =
     if n < 20 then vars.(n) else make (Var n)
 
   let var_index u =
@@ -227,7 +227,7 @@ module Level = struct
 end
 
 (** Level maps *)
-module LMap = struct 
+module LMap = struct
   module M = HMap.Make (Level)
   include M
 
@@ -242,8 +242,8 @@ module LMap = struct
       | _, _ -> Some r) l r
 
   let diff ext orig =
-    fold (fun u v acc -> 
-      if mem u orig then acc 
+    fold (fun u v acc ->
+      if mem u orig then acc
       else add u v acc)
       ext empty
 
@@ -288,22 +288,22 @@ module Universe =
 struct
   (* Invariants: non empty, sorted and without duplicates *)
 
-  module Expr = 
+  module Expr =
   struct
     type t = Level.t * int
 
     (* Hashing of expressions *)
-    module ExprHash = 
+    module ExprHash =
     struct
       type t = Level.t * int
       type u = Level.t -> Level.t
-      let hashcons hdir (b,n as x) = 
-	let b' = hdir b in 
-	  if b' == b then x else (b',n)
+      let hashcons hdir (b,n as x) =
+        let b' = hdir b in
+          if b' == b then x else (b',n)
       let eq l1 l2 =
-        l1 == l2 || 
+        l1 == l2 ||
         match l1,l2 with
-	| (b,n), (b',n') -> b == b' && n == n'
+        | (b,n), (b',n') -> b == b' && n == n'
 
       let hash (x, n) = n + Level.hash x
 
@@ -318,10 +318,10 @@ struct
 
     let compare u v =
       if u == v then 0
-      else 
-	let (x, n) = u and (x', n') = v in
-	  if Int.equal n n' then Level.compare x x'
-	  else n - n'
+      else
+        let (x, n) = u and (x', n') = v in
+          if Int.equal n n' then Level.compare x x'
+          else n - n'
 
     let sprop = hcons (Level.sprop, 0)
     let prop = hcons (Level.prop, 0)
@@ -334,29 +334,29 @@ struct
 
     let equal x y = x == y ||
       (let (u,n) = x and (v,n') = y in
-	 Int.equal n n' && Level.equal u v)
+         Int.equal n n' && Level.equal u v)
 
     let hash = ExprHash.hash
 
     let leq (u,n) (v,n') =
       let cmp = Level.compare u v in
-	if Int.equal cmp 0 then n <= n'
-	else if n <= n' then 
+        if Int.equal cmp 0 then n <= n'
+        else if n <= n' then
           (Level.is_prop u && not (Level.is_sprop v))
-	else false
+        else false
 
     let successor (u,n) =
       if Level.is_small u then type1
       else (u, n + 1)
 
-    let addn k (u,n as x) = 
-      if k = 0 then x 
+    let addn k (u,n as x) =
+      if k = 0 then x
       else if Level.is_small u then
-	(Level.set,n+k)
+        (Level.set,n+k)
       else (u,n+k)
 
     type super_result =
-	SuperSame of bool
+        SuperSame of bool
         (* The level expressions are in cumulativity relation. boolean
            indicates if left is smaller than right?  *)
       | SuperDiff of int
@@ -370,7 +370,7 @@ struct
     let super (u,n) (v,n') =
       let cmp = Level.compare u v in
         if Int.equal cmp 0 then SuperSame (n < n')
-	else
+        else
           let open RawLevel in
           match Level.data u, n, Level.data v, n' with
           | SProp, _, SProp, _ | Prop, _, Prop, _ -> SuperSame (n < n')
@@ -387,7 +387,7 @@ struct
 
     let pr x = str(to_string x)
 
-    let pr_with f (v, n) = 
+    let pr_with f (v, n) =
       if Int.equal n 0 then f v
       else f v ++ str"+" ++ int n
 
@@ -398,15 +398,15 @@ struct
     let level = function
       | (v,0) -> Some v
       | _ -> None
-	
+
     let get_level (v,_n) = v
 
-    let map f (v, n as x) = 
-      let v' = f v in 
-	if v' == v then x
-	else if Level.is_prop v' && n != 0 then
-	  (Level.set, n)
-	else (v', n)
+    let map f (v, n as x) =
+      let v' = f v in
+        if v' == v then x
+        else if Level.is_prop v' && n != 0 then
+          (Level.set, n)
+        else (v', n)
 
   end
 
@@ -432,16 +432,16 @@ struct
 
   let pr l = match l with
     | [u] -> Expr.pr u
-    | _ -> 
+    | _ ->
       str "max(" ++ hov 0
-	(prlist_with_sep pr_comma Expr.pr l) ++
+        (prlist_with_sep pr_comma Expr.pr l) ++
         str ")"
 
   let pr_with f l = match l with
     | [u] -> Expr.pr_with f u
-    | _ -> 
+    | _ ->
       str "max(" ++ hov 0
-	(prlist_with_sep pr_comma (Expr.pr_with f) l) ++
+        (prlist_with_sep pr_comma (Expr.pr_with f) l) ++
         str ")"
 
   let is_level l = match l with
@@ -456,10 +456,10 @@ struct
     | [l] -> Expr.level l
     | _ -> None
 
-  let levels l = 
+  let levels l =
     List.fold_left (fun acc x -> LSet.add (Expr.get_level x) acc) LSet.empty l
 
-  let is_small u = 
+  let is_small u =
     match u with
     | [l] -> Expr.is_small l
     | _ -> false
@@ -474,7 +474,7 @@ struct
   let type0 = tip Expr.set
 
   (* When typing [Prop] and [Set], there is no constraint on the level,
-     hence the definition of [type1_univ], the type of [Prop] *)    
+     hence the definition of [type1_univ], the type of [Prop] *)
   let type1 = tip Expr.type1
 
   let is_sprop x = equal sprop x
@@ -483,7 +483,7 @@ struct
 
   (* Returns the formal universe that lies just above the universe variable u.
      Used to type the sort u. *)
-  let super l = 
+  let super l =
     if is_small l then type1
     else
       List.Smart.map (fun x -> Expr.successor x) l
@@ -498,26 +498,26 @@ struct
     | h1 :: t1, h2 :: t2 ->
        let open Expr in
        (match super h1 h2 with
-	| SuperSame true (* h1 < h2 *) -> merge_univs t1 l2
-	| SuperSame false -> merge_univs l1 t2
-	| SuperDiff c ->
+        | SuperSame true (* h1 < h2 *) -> merge_univs t1 l2
+        | SuperSame false -> merge_univs l1 t2
+        | SuperDiff c ->
            if c <= 0 (* h1 < h2 is name order *)
-	   then cons h1 (merge_univs t1 l2)
-	   else cons h2 (merge_univs l1 t2))
+           then cons h1 (merge_univs t1 l2)
+           else cons h2 (merge_univs l1 t2))
 
   let sort u =
-    let rec aux a l = 
+    let rec aux a l =
       match l with
       | b :: l' ->
-	let open Expr in
+        let open Expr in
         (match super a b with
-	 | SuperSame false -> aux a l'
-	 | SuperSame true -> l
-	 | SuperDiff c ->
-	    if c <= 0 then cons a l
-	    else cons b (aux a l'))
+         | SuperSame false -> aux a l'
+         | SuperSame true -> l
+         | SuperDiff c ->
+            if c <= 0 then cons a l
+            else cons b (aux a l'))
       | [] -> cons a l
-    in 
+    in
       List.fold_right (fun a acc -> aux a acc) u []
 
   (* Returns the formal universe that is greater than the universes u and v.
@@ -578,11 +578,11 @@ exception UniverseInconsistency of univ_inconsistency
 let error_inconsistency o u v p =
   raise (UniverseInconsistency (o,make u,make v,p))
 
-(* Constraints and sets of constraints. *)    
+(* Constraints and sets of constraints. *)
 
 type univ_constraint = Level.t * constraint_type * Level.t
 
-let pr_constraint_type op = 
+let pr_constraint_type op =
   let op_str = match op with
     | Lt -> " < "
     | Le -> " <= "
@@ -601,8 +601,8 @@ struct
       else Level.compare v v'
 end
 
-module Constraint = 
-struct 
+module Constraint =
+struct
   module S = Set.Make(UConstraintOrd)
   include S
 
@@ -626,7 +626,7 @@ module Hconstraint =
       type u = universe_level -> universe_level
       let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
       let eq (l1,k,l2) (l1',k',l2') =
-	l1 == l1' && k == k' && l2 == l2'
+        l1 == l1' && k == k' && l2 == l2'
       let hash = Hashtbl.hash
     end)
 
@@ -636,11 +636,11 @@ module Hconstraints =
       type t = constraints
       type u = univ_constraint -> univ_constraint
       let hashcons huc s =
-	Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
+        Constraint.fold (fun x -> Constraint.add (huc x)) s Constraint.empty
       let eq s s' =
-	List.for_all2eq (==)
-	  (Constraint.elements s)
-	  (Constraint.elements s')
+        List.for_all2eq (==)
+          (Constraint.elements s)
+          (Constraint.elements s')
       let hash = Hashtbl.hash
     end)
 
@@ -659,7 +659,7 @@ type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
 let enforce_eq_level u v c =
   (* We discard trivial constraints like u=u *)
-  if Level.equal u v then c 
+  if Level.equal u v then c
   else if Level.apart u v then
     error_inconsistency Eq u v None
   else Constraint.add (u,Eq,v) c
@@ -680,24 +680,24 @@ let constraint_add_leq v u c =
   if Expr.equal v u then c
   else
     match v, u with
-    | (x,n), (y,m) -> 
+    | (x,n), (y,m) ->
     let j = m - n in
       if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
-	Constraint.add (x,Lt,y) c
+        Constraint.add (x,Lt,y) c
       else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
-	if Level.equal x y then (* u+(k+1) <= u *)
-	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None))
-	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
+        if Level.equal x y then (* u+(k+1) <= u *)
+          raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None))
+        else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
       else if j = 0 then
-	Constraint.add (x,Le,y) c
+        Constraint.add (x,Le,y) c
       else (* j >= 1 *) (* m = n + k, u <= v+k *)
-	if Level.equal x y then c (* u <= u+k, trivial *)
-	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
+        if Level.equal x y then c (* u <= u+k, trivial *)
+        else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
         else Constraint.add (x,Le,y) c (* u <= v implies u <= v+k *)
-	  
+
 let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
 
-let check_univ_leq u v = 
+let check_univ_leq u v =
   Universe.for_all (fun u -> check_univ_leq_one u v) u
 
 let enforce_leq u v c =
@@ -721,7 +721,7 @@ let enforce_leq_level u v c =
 let univ_level_mem u v =
   List.exists (fun (l, n) -> Int.equal n 0 && Level.equal u l) v
 
-let univ_level_rem u v min = 
+let univ_level_rem u v min =
   match Universe.level v with
   | Some u' -> if Level.equal u u' then min else v
   | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v
@@ -794,7 +794,7 @@ module Instance : sig
 
     val empty : t
     val is_empty : t -> bool
-      
+
     val of_array : Level.t array -> t
     val to_array : t -> Level.t array
 
@@ -808,10 +808,10 @@ module Instance : sig
     val share : t -> t * int
 
     val subst_fn : universe_level_subst_fn -> t -> t
-    
+
     val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
     val levels : t -> LSet.t
-end = 
+end =
 struct
   type t = Level.t array
 
@@ -822,53 +822,53 @@ struct
     type nonrec t = t
     type u = Level.t -> Level.t
 
-    let hashcons huniv a = 
+    let hashcons huniv a =
       let len = Array.length a in
-	if Int.equal len 0 then empty
-	else begin
-	  for i = 0 to len - 1 do
-	    let x = Array.unsafe_get a i in
-	    let x' = huniv x in
-	      if x == x' then ()
-	      else Array.unsafe_set a i x'
-	  done;
-	  a
-	end
+        if Int.equal len 0 then empty
+        else begin
+          for i = 0 to len - 1 do
+            let x = Array.unsafe_get a i in
+            let x' = huniv x in
+              if x == x' then ()
+              else Array.unsafe_set a i x'
+          done;
+          a
+        end
 
     let eq t1 t2 =
       t1 == t2 ||
-	(Int.equal (Array.length t1) (Array.length t2) &&
-	   let rec aux i =
-	     (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
-	   in aux 0)
-	
-    let hash a = 
+        (Int.equal (Array.length t1) (Array.length t2) &&
+           let rec aux i =
+             (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
+           in aux 0)
+
+    let hash a =
       let accu = ref 0 in
-	for i = 0 to Array.length a - 1 do
-	  let l = Array.unsafe_get a i in
-	  let h = Level.hash l in
-	    accu := Hashset.Combine.combine !accu h;
-	done;
-	(* [h] must be positive. *)
-	let h = !accu land 0x3FFFFFFF in
-	  h
+        for i = 0 to Array.length a - 1 do
+          let l = Array.unsafe_get a i in
+          let h = Level.hash l in
+            accu := Hashset.Combine.combine !accu h;
+        done;
+        (* [h] must be positive. *)
+        let h = !accu land 0x3FFFFFFF in
+          h
   end
 
   module HInstance = Hashcons.Make(HInstancestruct)
 
   let hcons = Hashcons.simple_hcons HInstance.generate HInstance.hcons Level.hcons
-    
+
   let hash = HInstancestruct.hash
-    
+
   let share a = (hcons a, hash a)
-	      
+
   let empty = hcons [||]
 
   let is_empty x = Int.equal (Array.length x) 0
 
   let append x y =
     if Array.length x = 0 then y
-    else if Array.length y = 0 then x 
+    else if Array.length y = 0 then x
     else Array.append x y
 
   let of_array a =
@@ -879,7 +879,7 @@ struct
 
   let length a = Array.length a
 
-  let subst_fn fn t = 
+  let subst_fn fn t =
     let t' = CArray.Smart.map fn t in
       if t' == t then t else of_array t'
 
@@ -892,20 +892,20 @@ struct
     in
     prvecti_with_sep spc ppu
 
-  let equal t u = 
+  let equal t u =
     t == u ||
       (Array.is_empty t && Array.is_empty u) ||
-      (CArray.for_all2 Level.equal t u 
-	 (* Necessary as universe instances might come from different modules and 
-	    unmarshalling doesn't preserve sharing *))
+      (CArray.for_all2 Level.equal t u
+         (* Necessary as universe instances might come from different modules and
+            unmarshalling doesn't preserve sharing *))
 
 end
 
-let enforce_eq_instances x y = 
+let enforce_eq_instances x y =
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
       anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with")
-		 (Pp.str " instances of different lengths."));
+                 (Pp.str " instances of different lengths."));
     CArray.fold_right2 enforce_eq_level ax ay
 
 let enforce_eq_variance_instances = Variance.eq_constraints
@@ -913,10 +913,10 @@ let enforce_leq_variance_instances = Variance.leq_constraints
 
 let subst_instance_level s l =
   match l.Level.data with
-  | Level.Var n -> s.(n) 
+  | Level.Var n -> s.(n)
   | _ -> l
 
-let subst_instance_instance s i = 
+let subst_instance_instance s i =
   Array.Smart.map (fun l -> subst_instance_level s l) i
 
 let subst_instance_universe s u =
@@ -932,9 +932,9 @@ let subst_instance_constraint s (u,d,v as c) =
     else (u',d,v')
 
 let subst_instance_constraints s csts =
-  Constraint.fold 
+  Constraint.fold
     (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
-    csts Constraint.empty 
+    csts Constraint.empty
 
 type 'a puniverses = 'a * Instance.t
 let out_punivs (x, _y) = x
@@ -1017,7 +1017,7 @@ let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} =
 let hcons_abstract_universe_context = AUContext.hcons
 
 (** A set of universes with universe constraints.
-    We linearize the set to a list after typechecking. 
+    We linearize the set to a list after typechecking.
     Beware, representation could change.
 *)
 
@@ -1030,7 +1030,7 @@ struct
 
   let equal (univs, cst as x) (univs', cst' as y) =
     x == y || (LSet.equal univs univs' && Constraint.equal cst cst')
-									
+
   let of_set s = (s, Constraint.empty)
   let singleton l = of_set (LSet.singleton l)
   let of_instance i = of_set (Instance.levels i)
@@ -1059,7 +1059,7 @@ struct
     let univs = Array.fold_left fold univs v in
     (univs, cst)
 
-  let sort_levels a = 
+  let sort_levels a =
     Array.sort Level.compare a; a
 
   let to_context (ctx, cst) =
@@ -1112,17 +1112,17 @@ let subst_univs_level_instance subst i =
   let i' = Instance.subst_fn (subst_univs_level_level subst) i in
     if i == i' then i
     else i'
-	
+
 let subst_univs_level_constraint subst (u,d,v) =
-  let u' = subst_univs_level_level subst u 
+  let u' = subst_univs_level_level subst u
   and v' = subst_univs_level_level subst v in
     if d != Lt && Level.equal u' v' then None
     else Some (u',d,v')
 
 let subst_univs_level_constraints subst csts =
-  Constraint.fold 
+  Constraint.fold
     (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
-    csts Constraint.empty 
+    csts Constraint.empty
 
 let subst_univs_level_abstract_universe_context subst (inst, csts) =
   inst, subst_univs_level_constraints subst csts
@@ -1136,41 +1136,41 @@ let subst_univs_expr_opt fn (l,n) =
   Universe.addn n (fn l)
 
 let subst_univs_universe fn ul =
-  let subst, nosubst = 
-    List.fold_right (fun u (subst,nosubst) -> 
+  let subst, nosubst =
+    List.fold_right (fun u (subst,nosubst) ->
       try let a' = subst_univs_expr_opt fn u in
-	    (a' :: subst, nosubst)
+            (a' :: subst, nosubst)
       with Not_found -> (subst, u :: nosubst))
       ul ([], [])
-  in 
+  in
     if CList.is_empty subst then ul
-    else 
-      let substs = 
-	List.fold_left Universe.merge_univs Universe.empty subst
+    else
+      let substs =
+        List.fold_left Universe.merge_univs Universe.empty subst
       in
-	List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
-	  substs nosubst
+        List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.tip u))
+          substs nosubst
 
-let make_instance_subst i = 
+let make_instance_subst i =
   let arr = Instance.to_array i in
     Array.fold_left_i (fun i acc l ->
       LMap.add l (Level.var i) acc)
       LMap.empty arr
 
-let make_inverse_instance_subst i = 
+let make_inverse_instance_subst i =
   let arr = Instance.to_array i in
     Array.fold_left_i (fun i acc l ->
       LMap.add (Level.var i) l acc)
       LMap.empty arr
 
-let make_abstract_instance (ctx, _) = 
+let make_abstract_instance (ctx, _) =
   Array.init (Array.length ctx) (fun i -> Level.var i)
 
 let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
   let () = assert (Int.equal (Array.length nas) (Instance.length instance)) in
   let subst = make_instance_subst instance in
-  let cstrs = subst_univs_level_constraints subst 
+  let cstrs = subst_univs_level_constraints subst
       (UContext.constraints ctx)
   in
   let ctx = (nas, cstrs) in
@@ -1200,28 +1200,28 @@ let pr_abstract_universe_context = AUContext.pr
 
 let pr_universe_context_set = ContextSet.pr
 
-let pr_universe_subst = 
+let pr_universe_subst =
   LMap.pr (fun u -> str" := " ++ Universe.pr u ++ spc ())
 
-let pr_universe_level_subst = 
+let pr_universe_level_subst =
   LMap.pr (fun u -> str" := " ++ Level.pr u ++ spc ())
 
-module Huniverse_set = 
+module Huniverse_set =
   Hashcons.Make(
     struct
       type t = universe_set
       type u = universe_level -> universe_level
       let hashcons huc s =
-	LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty
+        LSet.fold (fun x -> LSet.add (huc x)) s LSet.empty
       let eq s s' =
-	LSet.equal s s'
+        LSet.equal s s'
       let hash = Hashtbl.hash
     end)
 
-let hcons_universe_set = 
+let hcons_universe_set =
   Hashcons.simple_hcons Huniverse_set.generate Huniverse_set.hcons Level.hcons
 
-let hcons_universe_context_set (v, c) = 
+let hcons_universe_context_set (v, c) =
   (hcons_universe_set v, hcons_constraints c)
 
 let hcons_univ x = Universe.hcons x
@@ -1229,7 +1229,7 @@ let hcons_univ x = Universe.hcons x
 let explain_universe_inconsistency prl (o,u,v,p : univ_inconsistency) =
   let pr_uni = Universe.pr_with prl in
   let pr_rel = function
-    | Eq -> str"=" | Lt -> str"<" | Le -> str"<=" 
+    | Eq -> str"=" | Lt -> str"<" | Le -> str"<="
   in
   let reason = match p with
     | None -> mt()
diff --git a/kernel/vars.ml b/kernel/vars.ml
index dd187387d4..c2775a6896 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -164,7 +164,7 @@ let subst_of_rel_context_instance sign l =
     match sign, l with
     | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args'
     | LocalDef (_,c,_)::sign', args' ->
-	aux (substl subst c :: subst) sign' args'
+        aux (substl subst c :: subst) sign' args'
     | [], [] -> subst
     | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match.")
   in aux [] (List.rev sign) l
@@ -228,41 +228,41 @@ open Constr
 
 let subst_univs_level_constr subst c =
   if Univ.is_empty_level_subst subst then c
-  else 
+  else
     let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in
     let changed = ref false in
-    let rec aux t = 
+    let rec aux t =
       match kind t with
-      | Const (c, u) -> 
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; mkConstU (c, u'))
+      | Const (c, u) ->
+        if Univ.Instance.is_empty u then t
+        else
+          let u' = f u in
+            if u' == u then t
+            else (changed := true; mkConstU (c, u'))
       | Ind (i, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-	  let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; mkIndU (i, u'))
+        if Univ.Instance.is_empty u then t
+        else
+          let u' = f u in
+            if u' == u then t
+            else (changed := true; mkIndU (i, u'))
       | Construct (c, u) ->
-	if Univ.Instance.is_empty u then t
-	else 
-          let u' = f u in 
-	    if u' == u then t
-	    else (changed := true; mkConstructU (c, u'))
-      | Sort (Sorts.Type u) -> 
+        if Univ.Instance.is_empty u then t
+        else
+          let u' = f u in
+            if u' == u then t
+            else (changed := true; mkConstructU (c, u'))
+      | Sort (Sorts.Type u) ->
          let u' = Univ.subst_univs_level_universe subst u in
-	   if u' == u then t else 
-	     (changed := true; mkSort (Sorts.sort_of_univ u'))
+           if u' == u then t else
+             (changed := true; mkSort (Sorts.sort_of_univ u'))
       | _ -> Constr.map aux t
     in
     let c' = aux c in
       if !changed then c' else c
 
-let subst_univs_level_context s = 
+let subst_univs_level_context s =
   Context.Rel.map (subst_univs_level_constr s)
-      
+
 let subst_instance_constr subst c =
   if Univ.Instance.is_empty subst then c
   else
@@ -303,7 +303,7 @@ let univ_instantiate_constr u c =
 (* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
 (* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
 
-let subst_instance_context s ctx = 
+let subst_instance_context s ctx =
   if Univ.Instance.is_empty s then ctx
   else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 5d36ad54a2..3563407f7e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -65,11 +65,11 @@ and conv_whd env pb k whd1 whd2 cu =
       let tag1 = btag b1 and tag2 = btag b2 in
       let sz = bsize b1 in
       if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then
-	let rcu = ref cu in
-	for i = 0 to sz - 1 do
-	  rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu
-	done;
-	!rcu
+        let rcu = ref cu in
+        for i = 0 to sz - 1 do
+          rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu
+        done;
+        !rcu
       else raise NotConvertible
   | Vint64 i1, Vint64 i2 ->
     if Int64.equal i1 i2 then cu else raise NotConvertible
@@ -105,12 +105,12 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
           let u2 = Univ.Instance.of_array u2 in
           let cu = convert_instances ~flex:false u1 u2 cu in
           conv_arguments env ~from:ulen k args1 args2
-	    (conv_stack env k stk1' stk2' cu)
+            (conv_stack env k stk1' stk2' cu)
         | _, _ -> assert false (* Should not happen if problem is well typed *)
     else raise NotConvertible
   | Aid ik1, Aid ik2 ->
     if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
-	conv_stack env k stk1 stk2 cu
+        conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Asort s1, Asort s2 ->
     sort_cmp_universes env pb s1 s2 cu
@@ -123,17 +123,17 @@ and conv_stack env k stk1 stk2 cu =
       conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu)
   | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
       conv_stack env k stk1 stk2
-	(conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu))
+        (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu))
   | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
       if check_switch sw1 sw2 then
-	let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
-	let rcu = ref (conv_val env CONV k vt1 vt2 cu) in
-	let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
-	for i = 0 to Array.length b1 - 1 do
-	  rcu :=
-	    conv_val env CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu
-	done;
-	conv_stack env k stk1 stk2 !rcu
+        let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
+        let rcu = ref (conv_val env CONV k vt1 vt2 cu) in
+        let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
+        for i = 0 to Array.length b1 - 1 do
+          rcu :=
+            conv_val env CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu
+        done;
+        conv_stack env k stk1 stk2 !rcu
       else raise NotConvertible
   | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
     if Projection.Repr.equal p1 p2 then conv_stack env k stk1 stk2 cu
@@ -174,7 +174,7 @@ and conv_arguments env ?from:(from=0) k args1 args2 cu =
     if Int.equal n (nargs args2) then
       let rcu = ref cu in
       for i = from to n - 1 do
-	rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu
+        rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu
       done;
       !rcu
     else raise NotConvertible
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 5f08720f77..ee3e7a9913 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -21,8 +21,8 @@ let popstop_code i =
   else
     begin
       popstop_tbl :=
-	Array.init (i+10)
-	  (fun j -> if j < len then !popstop_tbl.(j) else mkPopStopCode j);
+        Array.init (i+10)
+          (fun j -> if j < len then !popstop_tbl.(j) else mkPopStopCode j);
       !popstop_tbl.(i)
     end
 
@@ -143,25 +143,25 @@ let rec apply_stack a stk v =
   | Zapp args :: stk -> apply_stack (apply_arguments (fun_of_val a) args) stk v
   | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v
   | Zfix(f,args) :: stk ->
-      let a,stk = 
-	match stk with
-	| Zapp args' :: stk ->
-	    push_ra stop;
-	    push_arguments args';
-	    push_val a;
-	    push_arguments args;
-	    let a =
+      let a,stk =
+        match stk with
+        | Zapp args' :: stk ->
+            push_ra stop;
+            push_arguments args';
+            push_val a;
+            push_arguments args;
+            let a =
               interprete (fix_code f) (fix_val f) (fix_env f)
-		(nargs args+ nargs args') in
-	    a, stk
-	| _ -> 
-	    push_ra stop;
-	    push_val a;
-	    push_arguments args;
-	    let a =
+                (nargs args+ nargs args') in
+            a, stk
+        | _ ->
+            push_ra stop;
+            push_val a;
+            push_arguments args;
+            let a =
               interprete (fix_code f) (fix_val f) (fix_env f)
-		(nargs args) in
-	    a, stk in
+                (nargs args) in
+            a, stk in
       apply_stack a stk v
   | Zswitch sw :: stk ->
       apply_stack (apply_switch sw a) stk v
@@ -172,7 +172,7 @@ let apply_whd k whd =
   | Vprod _ | Vconstr_const _ | Vconstr_block _ | Vint64 _ | Vfloat64 _ ->
      assert false
   | Vfun f -> reduce_fun k f
-  | Vfix(f, None) -> 
+  | Vfix(f, None) ->
       push_ra stop;
       push_val v;
       interprete (fix_code f) (fix_val f) (fix_env f) 0