Cosmetic: no more whitespace at end of lines in extraction files

(diff says it's a big commit, whereas diff -w says it's an empty one ;-)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11547 85f007b7-540e-0410-9357-904b9bb8a0f7

19 files changed, 1700 insertions, 1700 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index b23bbeac4..11c3b3b5b 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -33,31 +33,31 @@ let pr_binding = function
   | [] -> mt ()
   | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
 
-let fnl2 () = fnl () ++ fnl () 
+let fnl2 () = fnl () ++ fnl ()
 
 let space_if = function true -> str " " | false -> mt ()
 
 let sec_space_if = function true -> spc () | false -> mt ()
 
-let is_digit = function 
+let is_digit = function
   | '0'..'9' -> true
   | _ -> false
 
-let begins_with_CoqXX s = 
-  let n = String.length s in 
+let begins_with_CoqXX s =
+  let n = String.length s in
   n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
-  let i = ref 3 in 
+  let i = ref 3 in
   try while !i < n do
     if s.[!i] = '_' then i:=n (*Stop*)
-    else if is_digit s.[!i] then incr i 
+    else if is_digit s.[!i] then incr i
     else raise Not_found
   done; true
   with Not_found -> false
-  
-let unquote s = 
-  if lang () <> Scheme then s 
-  else 
-    let s = String.copy s in 
+
+let unquote s =
+  if lang () <> Scheme then s
+  else
+    let s = String.copy s in
     for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
     s
 
@@ -91,11 +91,11 @@ type env = identifier list * Idset.t
 
 (*s Generic renaming issues for local variable names. *)
 
-let rec rename_id id avoid = 
+let rec rename_id id avoid =
   if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
 
 let rec rename_vars avoid = function
-  | [] -> 
+  | [] ->
       [], avoid
   | id :: idl when id == dummy_name ->
       (* we don't rename dummy binders *)
@@ -106,12 +106,12 @@ let rec rename_vars avoid = function
       let id = rename_id (lowercase_id id) avoid in
       (id :: idl, Idset.add id avoid)
 
-let rename_tvars avoid l = 
-  let rec rename avoid = function 
-    | [] -> [],avoid 
-    | id :: idl -> 
-	let id = rename_id (lowercase_id id) avoid in 
-	let idl, avoid = rename (Idset.add id avoid) idl in 
+let rename_tvars avoid l =
+  let rec rename avoid = function
+    | [] -> [],avoid
+    | id :: idl ->
+	let id = rename_id (lowercase_id id) avoid in
+	let idl, avoid = rename (Idset.add id avoid) idl in
 	(id :: idl, avoid) in
   fst (rename avoid l)
 
@@ -119,8 +119,8 @@ let push_vars ids (db,avoid) =
   let ids',avoid' = rename_vars avoid ids in
   ids', (ids' @ db, avoid')
 
-let get_db_name n (db,_) = 
-  let id = List.nth db (pred n) in 
+let get_db_name n (db,_) =
+  let id = List.nth db (pred n) in
   if id = dummy_name then id_of_string "__" else id
 
 
@@ -175,14 +175,14 @@ let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
 (*s table indicating the visible horizon at a precise moment,
     i.e. the stack of structures we are inside.
 
-  - The sequence of [mp] parts should have the following form: 
-  [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either 
-  be a [MPdot] over the last entry, or something new, mainly 
+  - The sequence of [mp] parts should have the following form:
+  [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either
+  be a [MPdot] over the last entry, or something new, mainly
   [MPself], or [MPfile] at the beginning.
 
   - The [content] part is used to recoard all the names already
   seen at this level.
-  
+
   - The [subst] part is here mainly for printing signature
   (in which names are still short, i.e. relative to a [msid]).
 *)
@@ -234,9 +234,9 @@ let reset_renaming_tables flag =
 
 (*S Renaming functions *)
 
-(* This function creates from [id] a correct uppercase/lowercase identifier. 
-   This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes 
-   with previous [Coq_id] variable, these prefixes are duplicated if already 
+(* This function creates from [id] a correct uppercase/lowercase identifier.
+   This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes
+   with previous [Coq_id] variable, these prefixes are duplicated if already
    existing. *)
 
 let modular_rename k id =
@@ -250,7 +250,7 @@ let modular_rename k id =
   then prefix ^ s
   else s
 
-(*s For monolithic extraction, first-level modules might have to be renamed 
+(*s For monolithic extraction, first-level modules might have to be renamed
     with unique numbers *)
 
 let modfstlev_rename =
@@ -318,8 +318,8 @@ let ref_renaming =
 
 (* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
    can be printed as [s] in the current context of visible
-   modules. More precisely, we check if there exists a 
-   visible [mp] that contains [s]. 
+   modules. More precisely, we check if there exists a
+   visible [mp] that contains [s].
    The verification stops if we encounter [mp=mp0]. *)
 
 let rec clash mem mp0 ks = function
@@ -362,8 +362,8 @@ let opened_libraries () =
 (*s On-the-fly qualification issues for both monolithic or modular extraction. *)
 
 (* First, a function that factorize the printing of both [global_reference]
-   and module names for ocaml. When [k=Mod] then [olab=None], otherwise it 
-   contains the label of the reference to print. 
+   and module names for ocaml. When [k=Mod] then [olab=None], otherwise it
+   contains the label of the reference to print.
    Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *)
 
 let pp_gen k mp ls olab =
@@ -376,7 +376,7 @@ let pp_gen k mp ls olab =
     (* Reference r / module path mp is of the form [<prefix>.s.<List.rev ls'>].
        Difficulty: in ocaml the prefix part cannot be used for
        qualification (we are inside it) and the rest of the long
-       name may be hidden. 
+       name may be hidden.
        Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *)
     let k' = if ls' = [] then k else Mod in
     if visible_clash prefix (k',s) then
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 38fd863c5..c401bd059 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -19,7 +19,7 @@ val space_if : bool -> std_ppcmds
 val sec_space_if : bool -> std_ppcmds
 
 val pp_par : bool -> std_ppcmds -> std_ppcmds
-val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds 
+val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
 val pr_binding : identifier list -> std_ppcmds
 
 val rename_id : identifier -> Idset.t -> identifier
@@ -28,7 +28,7 @@ type env = identifier list * Idset.t
 val empty_env : unit -> env
 
 val rename_vars: Idset.t -> identifier list -> env
-val rename_tvars: Idset.t -> identifier list -> identifier list 
+val rename_tvars: Idset.t -> identifier list -> identifier list
 val push_vars : identifier list -> env -> identifier list * env
 val get_db_name : int -> env -> identifier
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 6d2b332ab..034d07c0e 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -201,8 +201,8 @@ and extract_seb_spec env = function
       MTwith(extract_seb_spec env mtb',
 	     ML_With_module(idl,mp))
 (* TODO: On pourrait peut-etre oter certaines eta-expansion, du genre:
-   | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_)) 
-     when mbid = mbid2 -> extract_seb_spec env m 
+   | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_))
+     when mbid = mbid2 -> extract_seb_spec env m
    (* faudrait alors ajouter un test de non-apparition de mbid dans mb *)
 *)
   | SEBfunctor (mbid, mtb, mtb') ->
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index bf470d096..dcb4601e5 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -19,5 +19,5 @@ val extraction_library : bool -> identifier -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
 
-val mono_environment : 
+val mono_environment :
  global_reference list -> module_path list -> Miniml.ml_structure
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f9e2799a1..a4d2445ec 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -44,18 +44,18 @@ let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None
 
 (*S Generation of flags and signatures. *)
 
-(* The type [flag] gives us information about any Coq term: 
+(* The type [flag] gives us information about any Coq term:
    \begin{itemize}
-   \item [TypeScheme] denotes a type scheme, that is 
-     something that will become a type after enough applications. 
-     More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with 
-     [s = Set], [Prop] or [Type] 
-   \item [Default] denotes the other cases. It may be inexact after 
+   \item [TypeScheme] denotes a type scheme, that is
+     something that will become a type after enough applications.
+     More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with
+     [s = Set], [Prop] or [Type]
+   \item [Default] denotes the other cases. It may be inexact after
      instanciation. For example [(X:Type)X] is [Default] and may give [Set]
      after instanciation, which is rather [TypeScheme]
    \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
-   \item [Info] is the opposite. The same example [(X:Type)X] shows 
-     that an [Info] term might in fact be [Logic] later on. 
+   \item [Info] is the opposite. The same example [(X:Type)X] shows
+     that an [Info] term might in fact be [Logic] later on.
    \end{itemize} *)
 
 type info = Logic | Info
@@ -64,11 +64,11 @@ type scheme = TypeScheme | Default
 
 type flag = info * scheme
 
-(*s [flag_of_type] transforms a type [t] into a [flag]. 
+(*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
-let rec flag_of_type env t = 
-  let t = whd_betadeltaiota env none t in 
+let rec flag_of_type env t =
+  let t = whd_betadeltaiota env none t in
   match kind_of_term t with
     | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
     | Sort (Prop Null) -> (Logic,TypeScheme)
@@ -81,8 +81,8 @@ let is_default env t = (flag_of_type env t = (Info, Default))
 
 exception NotDefault of kill_reason
 
-let check_default env t = 
-  match flag_of_type env t with 
+let check_default env t =
+  match flag_of_type env t with
     | _,TypeScheme -> raise (NotDefault Ktype)
     | Logic,_ -> raise (NotDefault Kother)
     | _ -> ()
@@ -91,17 +91,17 @@ let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
 
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
-let rec type_sign env c = 
+let rec type_sign env c =
   match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
+    | Prod (n,t,d) ->
 	(if is_info_scheme env t then Keep else Kill Kother)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
-let rec type_scheme_nb_args env c = 
+let rec type_scheme_nb_args env c =
   match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
-	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in 
+    | Prod (n,t,d) ->
+	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
 	if is_info_scheme env t then n+1 else n
     | _ -> 0
 
@@ -109,128 +109,128 @@ let _ = register_type_scheme_nb_args type_scheme_nb_args
 
 (*s [type_sign_vl] does the same, plus a type var list. *)
 
-let rec type_sign_vl env c = 
+let rec type_sign_vl env c =
   match kind_of_term (whd_betadeltaiota env none c) with
-    | Prod (n,t,d) -> 
-	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in 
+    | Prod (n,t,d) ->
+	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kother::s, vl
 	else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
     | _ -> [],[]
 
-let rec nb_default_params env c = 
+let rec nb_default_params env c =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
-	let n = nb_default_params (push_rel_assum (n,t) env) d in 
+	let n = nb_default_params (push_rel_assum (n,t) env) d in
 	if is_default env t then n+1 else n
     | _ -> 0
 
 (*S Management of type variable contexts. *)
 
-(* A De Bruijn variable context (db) is a context for translating Coq [Rel]  
+(* A De Bruijn variable context (db) is a context for translating Coq [Rel]
    into ML type [Tvar]. *)
 
 (*s From a type signature toward a type variable context (db). *)
 
-let db_from_sign s = 
-  let rec make i acc = function 
-    | [] -> acc  
+let db_from_sign s =
+  let rec make i acc = function
+    | [] -> acc
     | Keep :: l -> make (i+1) (i::acc) l
     | Kill _ :: l -> make i (0::acc) l
   in make 1 [] s
 
-(*s Create a type variable context from indications taken from 
-  an inductive type (see just below). *) 
+(*s Create a type variable context from indications taken from
+  an inductive type (see just below). *)
 
-let rec db_from_ind dbmap i = 
+let rec db_from_ind dbmap i =
   if i = 0 then []
   else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
 
-(*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument 
+(*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
   of a constructor corresponds to the j-th type var of the ML inductive. *)
 
 (* \begin{itemize}
    \item [si] : signature of the inductive
-   \item [i] :  counter of Coq args for [(I args)] 
-   \item [j] : counter of ML type vars 
-   \item [relmax] : total args number of the constructor 
+   \item [i] :  counter of Coq args for [(I args)]
+   \item [j] : counter of ML type vars
+   \item [relmax] : total args number of the constructor
    \end{itemize} *)
 
-let parse_ind_args si args relmax = 
-  let rec parse i j = function 
+let parse_ind_args si args relmax =
+  let rec parse i j = function
     | [] -> Intmap.empty
     | Kill _ :: s -> parse (i+1) j s
-    | Keep :: s -> 
-      (match kind_of_term args.(i-1) with 
+    | Keep :: s ->
+      (match kind_of_term args.(i-1) with
 	 | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
 	 | _ -> parse (i+1) (j+1) s)
-  in parse 1 1 si 
+  in parse 1 1 si
 
 (*S Extraction of a type. *)
 
-(* [extract_type env db c args] is used to produce an ML type from the 
+(* [extract_type env db c args] is used to produce an ML type from the
    coq term [(c args)], which is supposed to be a Coq type. *)
 
 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-(* [j] stands for the next ML type var. [j=0] means we do not 
-   generate ML type var anymore (in subterms for example). *) 
+(* [j] stands for the next ML type var. [j=0] means we do not
+   generate ML type var anymore (in subterms for example). *)
 
 
-let rec extract_type env db j c args = 
+let rec extract_type env db j c args =
   match kind_of_term (whd_betaiotazeta c) with
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
-    | Lambda (_,_,d) -> 
-	(match args with 
+    | Lambda (_,_,d) ->
+	(match args with
 	   | [] -> assert false (* otherwise the lambda would be reductible. *)
 	   | a :: args -> extract_type env db j (subst1 a d) args)
     | Prod (n,t,d) ->
-	assert (args = []); 
-	let env' = push_rel_assum (n,t) env in 
-	(match flag_of_type env t with 
-	   | (Info, Default) -> 
+	assert (args = []);
+	let env' = push_rel_assum (n,t) env in
+	(match flag_of_type env t with
+	   | (Info, Default) ->
 	       (* Standard case: two [extract_type] ... *)
-	       let mld = extract_type env' (0::db) j d [] in 
-	       (match expand env mld with 
+	       let mld = extract_type env' (0::db) j d [] in
+	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ -> Tarr (extract_type env db 0 t [], mld))
-	   | (Info, TypeScheme) when j > 0 -> 
+	   | (Info, TypeScheme) when j > 0 ->
 	       (* A new type var. *)
-	       let mld = extract_type env' (j::db) (j+1) d [] in 
-	       (match expand env mld with 
+	       let mld = extract_type env' (j::db) (j+1) d [] in
+	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ -> Tarr (Tdummy Ktype, mld))
-	   | _,lvl -> 
-	       let mld = extract_type env' (0::db) j d [] in 
-	       (match expand env mld with 
+	   | _,lvl ->
+	       let mld = extract_type env' (0::db) j d [] in
+	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
-		  | _ -> 
+		  | _ ->
 		      let reason = if lvl=TypeScheme then Ktype else Kother in
 		      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
     | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother
-    | Rel n -> 
+    | Rel n ->
 	(match lookup_rel n env with
            | (_,Some t,_) -> extract_type env db j (lift n t) args
-	   | _ -> 
+	   | _ ->
 	       (* Asks [db] a translation for [n]. *)
-	       if n > List.length db then Tunknown 
-	       else let n' = List.nth db (n-1) in 
+	       if n > List.length db then Tunknown
+	       else let n' = List.nth db (n-1) in
 	       if n' = 0 then Tunknown else Tvar n')
-    | Const kn -> 
-	let r = ConstRef kn in 
-	let cb = lookup_constant kn env in 
-	let typ = Typeops.type_of_constant_type env cb.const_type in 
-	(match flag_of_type env typ with 
-	   | (Info, TypeScheme) -> 
-	       let mlt = extract_type_app env db (r, type_sign env typ) args in 
-	       (match cb.const_body with 
+    | Const kn ->
+	let r = ConstRef kn in
+	let cb = lookup_constant kn env in
+	let typ = Typeops.type_of_constant_type env cb.const_type in
+	(match flag_of_type env typ with
+	   | (Info, TypeScheme) ->
+	       let mlt = extract_type_app env db (r, type_sign env typ) args in
+	       (match cb.const_body with
 		  | None -> mlt
-		  | Some _ when is_custom r -> mlt 
-		  | Some lbody -> 
-		      let newc = applist (Declarations.force lbody, args) in 
-		      let mlt' = extract_type env db j newc [] in 
+		  | Some _ when is_custom r -> mlt
+		  | Some lbody ->
+		      let newc = applist (Declarations.force lbody, args) in
+		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
 		      (* reduction, so [mlt] and [mlt'] might be different: *)
 		      (* The more precise is [mlt'], extracted after reduction *)
@@ -238,34 +238,34 @@ let rec extract_type env db j c args =
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
 		      if expand env mlt = expand env mlt' then mlt else mlt')
 	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
-	       (match cb.const_body with 
+	       (match cb.const_body with
 		  | None -> Tunknown (* Brutal approximation ... *)
-		  | Some lbody -> 
+		  | Some lbody ->
 		      (* We try to reduce. *)
-		      let newc = applist (Declarations.force lbody, args) in 
+		      let newc = applist (Declarations.force lbody, args) in
 		      extract_type env db j newc []))
     | Ind (kn,i) ->
-	let s = (extract_ind env kn).ind_packets.(i).ip_sign in  
+	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
 	extract_type_app env db (IndRef (kn,i),s) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
     | _ -> assert false
 
-(* [extract_maybe_type] calls [extract_type] when used on a Coq type, 
+(* [extract_maybe_type] calls [extract_type] when used on a Coq type,
    and otherwise returns [Tdummy] or [Tunknown] *)
 
-and extract_maybe_type env db c = 
-  let t = whd_betadeltaiota env none (type_of env c) in 
-  if isSort t then extract_type env db 0 c [] 
+and extract_maybe_type env db c =
+  let t = whd_betadeltaiota env none (type_of env c) in
+  if isSort t then extract_type env db 0 c []
   else if sort_of env t = InProp then Tdummy Kother else Tunknown
 
-(*s Auxiliary function dealing with type application. 
-  Precondition: [r] is a type scheme represented by the signature [s], 
+(*s Auxiliary function dealing with type application.
+  Precondition: [r] is a type scheme represented by the signature [s],
   and is completely applied: [List.length args = List.length s]. *)
-		  
+
 and extract_type_app env db (r,s) args =
-  let ml_args = 
-    List.fold_right 
-      (fun (b,c) a -> if b=Keep then 
+  let ml_args =
+    List.fold_right
+      (fun (b,c) a -> if b=Keep then
 	 let p = List.length (fst (splay_prod env none (type_of env c))) in
          let db = iterate (fun l -> 0 :: l) p db in
          (extract_type_scheme env db c p) :: a
@@ -276,23 +276,23 @@ and extract_type_app env db (r,s) args =
 (*S Extraction of a type scheme. *)
 
 (* [extract_type_scheme env db c p] works on a Coq term [c] which is
-  an informative type scheme. It means that [c] is not a Coq type, but will 
-  be when applied to sufficiently many arguments ([p] in fact).  
+  an informative type scheme. It means that [c] is not a Coq type, but will
+  be when applied to sufficiently many arguments ([p] in fact).
   This function decomposes p lambdas, with eta-expansion if needed. *)
 
 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
-and extract_type_scheme env db c p = 
-  if p=0 then extract_type env db 0 c [] 
-  else 
-    let c = whd_betaiotazeta c in 
-    match kind_of_term c with 
-      | Lambda (n,t,d) -> 
+and extract_type_scheme env db c p =
+  if p=0 then extract_type env db 0 c []
+  else
+    let c = whd_betaiotazeta c in
+    match kind_of_term c with
+      | Lambda (n,t,d) ->
           extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
-      | _ ->  
+      | _ ->
           let rels = fst (splay_prod env none (type_of env c)) in
-          let env = push_rels_assum rels env in  
-          let eta_args = List.rev_map mkRel (interval 1 p) in 
+          let env = push_rels_assum rels env in
+          let eta_args = List.rev_map mkRel (interval 1 p) in
           extract_type env db 0 (lift p c) eta_args
 
 
@@ -302,174 +302,174 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
   let mib = Environ.lookup_mind kn env in
   try
     (* For a same kn, we can get various bodies due to module substitutions.
-       We hence check that the mib has not changed from recording 
+       We hence check that the mib has not changed from recording
        time to retrieving time. Ideally we should also check the env. *)
-    let (mib0,ml_ind) = lookup_ind kn in 
-    if not (mib = mib0) then raise Not_found; 
+    let (mib0,ml_ind) = lookup_ind kn in
+    if not (mib = mib0) then raise Not_found;
     ml_ind
-  with Not_found -> 
+  with Not_found ->
     (* First, if this inductive is aliased via a Module, *)
     (* we process the original inductive. *)
-    Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; 
+    Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv;
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
-    let mip0 = mib.mind_packets.(0) in 
+    let mip0 = mib.mind_packets.(0) in
     let npar = mib.mind_nparams in
     let epar = push_rel_context mib.mind_params_ctxt env in
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
-    let packets = 
-      Array.map 
+    let packets =
+      Array.map
 	(fun mip ->
 	   let b = snd (mind_arity mip) <> InProp in
 	   let ar = Inductive.type_of_inductive env (mib,mip) in
 	   let s,v = if b then type_sign_vl env ar else [],[] in
-	   let t = Array.make (Array.length mip.mind_nf_lc) [] in 
+	   let t = Array.make (Array.length mip.mind_nf_lc) [] in
 	   { ip_typename = mip.mind_typename;
 	     ip_consnames = mip.mind_consnames;
-	     ip_logical = (not b); 
-	     ip_sign = s; 
-	     ip_vars = v; 
-	     ip_types = t }) 
-	mib.mind_packets 
-    in 
+	     ip_logical = (not b);
+	     ip_sign = s;
+	     ip_vars = v;
+	     ip_types = t })
+	mib.mind_packets
+    in
     add_ind kn mib
-      {ind_info = Standard; 
-       ind_nparams = npar; 
-       ind_packets = packets; 
-       ind_equiv = match mib.mind_equiv with 
-         | None -> NoEquiv 
+      {ind_info = Standard;
+       ind_nparams = npar;
+       ind_packets = packets;
+       ind_equiv = match mib.mind_equiv with
+         | None -> NoEquiv
 	 | Some kn -> Equiv kn
       };
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
-      let p = packets.(i) in 
+      let p = packets.(i) in
       if not p.ip_logical then
-	let types = arities_of_constructors env (kn,i) in 
-	for j = 0 to Array.length types - 1 do 
+	let types = arities_of_constructors env (kn,i) in
+	for j = 0 to Array.length types - 1 do
 	  let t = snd (decompose_prod_n npar types.(j)) in
-	  let prods,head = dest_prod epar t in 
-	  let nprods = List.length prods in 
+	  let prods,head = dest_prod epar t in
+	  let nprods = List.length prods in
           let args = match kind_of_term head with
             | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
             | _ -> [||]
           in
-	  let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in 
-	  let db = db_from_ind dbmap npar in 
+	  let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
+	  let db = db_from_ind dbmap npar in
 	  p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1)
 	done
     done;
     (* Third pass: we determine special cases. *)
-    let ind_info = 
-      try 
-	if not mib.mind_finite then raise (I Coinductive); 
-	if mib.mind_ntypes <> 1 then raise (I Standard); 
-	let p = packets.(0) in 
+    let ind_info =
+      try
+	if not mib.mind_finite then raise (I Coinductive);
+	if mib.mind_ntypes <> 1 then raise (I Standard);
+	let p = packets.(0) in
 	if p.ip_logical then raise (I Standard);
 	if Array.length p.ip_types <> 1 then raise (I Standard);
-	let typ = p.ip_types.(0) in 
-	let l = List.filter (fun t -> not (isDummy (expand env t))) typ in 
-	if List.length l = 1 && not (type_mem_kn kn (List.hd l)) 
-	then raise (I Singleton); 
+	let typ = p.ip_types.(0) in
+	let l = List.filter (fun t -> not (isDummy (expand env t))) typ in
+	if List.length l = 1 && not (type_mem_kn kn (List.hd l))
+	then raise (I Singleton);
 	if l = [] then raise (I Standard);
 	if not mib.mind_record then raise (I Standard);
-	let ip = (kn, 0) in 
-	let r = IndRef ip in 
-	if is_custom r then raise (I Standard); 
+	let ip = (kn, 0) in
+	let r = IndRef ip in
+	if is_custom r then raise (I Standard);
 	(* Now we're sure it's a record. *)
 	(* First, we find its field names. *)
-	let rec names_prod t = match kind_of_term t with 
+	let rec names_prod t = match kind_of_term t with
 	  | Prod(n,_,t) -> n::(names_prod t)
 	  | LetIn(_,_,_,t) -> names_prod t
 	  | Cast(t,_,_) -> names_prod t
 	  | _ -> []
-	in 
-	let field_names = 
-	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
+	in
+	let field_names =
+	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
 	assert (List.length field_names = List.length typ);
-	let projs = ref Cset.empty in 
-	let mp,d,_ = repr_kn kn in 
-	let rec select_fields l typs = match l,typs with 
+	let projs = ref Cset.empty in
+	let mp,d,_ = repr_kn kn in
+	let rec select_fields l typs = match l,typs with
 	  | [],[] -> []
-	  | (Name id)::l, typ::typs -> 
-	      if isDummy (expand env typ) then select_fields l typs 
-	      else  
-		let knp = make_con mp d (label_of_id id) in 
+	  | (Name id)::l, typ::typs ->
+	      if isDummy (expand env typ) then select_fields l typs
+	      else
+		let knp = make_con mp d (label_of_id id) in
 		if not (List.exists isKill (type2signature env typ))
-		then 
-		  projs := Cset.add knp !projs; 
+		then
+		  projs := Cset.add knp !projs;
 		(ConstRef knp) :: (select_fields l typs)
-	  | Anonymous::l, typ::typs -> 
+	  | Anonymous::l, typ::typs ->
 	      if isDummy (expand env typ) then select_fields l typs
 	      else error_record r
-	  | _ -> assert false 
-	in 
+	  | _ -> assert false
+	in
 	let field_glob = select_fields field_names typ
 	in
 	(* Is this record officially declared with its projections ? *)
 	(* If so, we use this information. *)
-	begin try 
+	begin try
 	  let n = nb_default_params env
             (Inductive.type_of_inductive env (mib,mip0))
 	  in
-	  List.iter 
-	    (Option.iter 
+	  List.iter
+	    (Option.iter
 	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))
 	    (lookup_projections ip)
 	with Not_found -> ()
-	end; 
+	end;
 	Record field_glob
       with (I info) -> info
     in
-    let i = {ind_info = ind_info; 
-	     ind_nparams = npar; 
-	     ind_packets = packets; 
-	     ind_equiv = match mib.mind_equiv with 
+    let i = {ind_info = ind_info;
+	     ind_nparams = npar;
+	     ind_packets = packets;
+	     ind_equiv = match mib.mind_equiv with
 	       | None -> NoEquiv
 	       | Some kn -> Equiv kn }
     in
-    add_ind kn mib i; 
+    add_ind kn mib i;
     i
 
-(*s [extract_type_cons] extracts the type of an inductive 
+(*s [extract_type_cons] extracts the type of an inductive
   constructor toward the corresponding list of ML types. *)
 
 (* \begin{itemize}
-   \item [db] is a context for translating Coq [Rel] into ML type [Tvar] 
+   \item [db] is a context for translating Coq [Rel] into ML type [Tvar]
    \item [dbmap] is a translation map (produced by a call to [parse_in_args])
-   \item [i] is the rank of the current product (initially [params_nb+1]) 
+   \item [i] is the rank of the current product (initially [params_nb+1])
    \end{itemize} *)
 
 and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_betadeltaiota env none c) with 
-    | Prod (n,t,d) -> 
+  match kind_of_term (whd_betadeltaiota env none c) with
+    | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
 	let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
-	let l = extract_type_cons env' db' dbmap d (i+1) in 
-	(extract_type env db 0 t []) :: l 
-    | _ -> [] 
+	let l = extract_type_cons env' db' dbmap d (i+1) in
+	(extract_type env db 0 t []) :: l
+    | _ -> []
 
 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
 
-and mlt_env env r = match r with 
-  | ConstRef kn -> 
-      (try 
-	 if not (visible_con kn) then raise Not_found; 
-	 match lookup_term kn with 
+and mlt_env env r = match r with
+  | ConstRef kn ->
+      (try
+	 if not (visible_con kn) then raise Not_found;
+	 match lookup_term kn with
 	   | Dtype (_,vl,mlt) -> Some mlt
 	   | _ -> None
-       with Not_found -> 
+       with Not_found ->
 	 let cb = Environ.lookup_constant kn env in
-	 let typ = Typeops.type_of_constant_type env cb.const_type in 
+	 let typ = Typeops.type_of_constant_type env cb.const_type in
 	 match cb.const_body with
 	   | None -> None
-	   | Some l_body -> 
-	       (match flag_of_type env typ with 
-		  | Info,TypeScheme -> 
+	   | Some l_body ->
+	       (match flag_of_type env typ with
+		  | Info,TypeScheme ->
 		      let body = Declarations.force l_body in
-		      let s,vl = type_sign_vl env typ in 
-		      let db = db_from_sign s in 
-		      let t = extract_type_scheme env db body (List.length s) 
+		      let s,vl = type_sign_vl env typ in
+		      let db = db_from_sign s in
+		      let t = extract_type_scheme env db body (List.length s)
 		      in add_term kn (Dtype (r, vl, t)); Some t
 		  | _ -> None))
   | _ -> None
@@ -481,15 +481,15 @@ let type_expunge env = type_expunge (mlt_env env)
 
 (*s Extraction of the type of a constant. *)
 
-let record_constant_type env kn opt_typ = 
-  try 
-    if not (visible_con kn) then raise Not_found; 
-    lookup_type kn 
+let record_constant_type env kn opt_typ =
+  try
+    if not (visible_con kn) then raise Not_found;
+    lookup_type kn
   with Not_found ->
-    let typ = match opt_typ with 
+    let typ = match opt_typ with
       | None -> Typeops.type_of_constant env kn
-      | Some typ -> typ 
-    in let mlt = extract_type env [] 1 typ [] 
+      | Some typ -> typ
+    in let mlt = extract_type env [] 1 typ []
     in let schema = (type_maxvar mlt, mlt)
     in add_type kn schema; schema
 
@@ -500,40 +500,40 @@ let record_constant_type env kn opt_typ =
 (* [mle] is a ML environment [Mlenv.t]. *)
 (* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
 
-let rec extract_term env mle mlt c args = 
+let rec extract_term env mle mlt c args =
   match kind_of_term c with
     | App (f,a) ->
 	extract_term env mle mlt f (Array.to_list a @ args)
     | Lambda (n, t, d) ->
-	let id = id_of_name n in 
-	(match args with 
-	   | a :: l -> 
+	let id = id_of_name n in
+	(match args with
+	   | a :: l ->
 	       (* We make as many [LetIn] as possible. *)
  	       let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l))
 	       in extract_term env mle mlt d' []
-	   | [] -> 
-	       let env' = push_rel_assum (Name id, t) env in 
+	   | [] ->
+	       let env' = push_rel_assum (Name id, t) env in
 	       let id, a = try check_default env t; id, new_meta()
 	       with NotDefault d -> dummy_name, Tdummy d
-	       in 
-	       let b = new_meta () in 
+	       in
+	       let b = new_meta () in
 	       (* If [mlt] cannot be unified with an arrow type, then magic! *)
-	       let magic = needs_magic (mlt, Tarr (a, b)) in 
-	       let d' = extract_term env' (Mlenv.push_type mle a) b d [] in 
+	       let magic = needs_magic (mlt, Tarr (a, b)) in
+	       let d' = extract_term env' (Mlenv.push_type mle a) b d [] in
 	       put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
-	let id = id_of_name n in 
-	let env' = push_rel (Name id, Some c1, t1) env in 
-	let args' = List.map (lift 1) args in 
-	(try 
-	  check_default env t1; 
-	  let a = new_meta () in 
+	let id = id_of_name n in
+	let env' = push_rel (Name id, Some c1, t1) env in
+	let args' = List.map (lift 1) args in
+	(try
+	  check_default env t1;
+	  let a = new_meta () in
 	  let c1' = extract_term env mle a c1 [] in
 	  (* The type of [c1'] is generalized and stored in [mle]. *)
-	  let mle' = Mlenv.push_gen mle a in 
-	  MLletin (id, c1', extract_term env' mle' mlt c2 args') 
-	with NotDefault d -> 
-	  let mle' = Mlenv.push_std_type mle (Tdummy d) in 
+	  let mle' = Mlenv.push_gen mle a in
+	  MLletin (id, c1', extract_term env' mle' mlt c2 args')
+	with NotDefault d ->
+	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
 	  ast_pop (extract_term env' mle' mlt c2 args'))
     | Const kn ->
 	extract_cst_app env mle mlt kn args
@@ -543,104 +543,104 @@ let rec extract_term env mle mlt c args =
 	(* As soon as the expected [mlt] for the head is known, *)
 	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
 	let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
-	in extract_app env mle mlt extract_rel args 
+	in extract_app env mle mlt extract_rel args
     | Case ({ci_ind=ip},_,c0,br) ->
  	extract_app env mle mlt (extract_case env mle (ip,c0,br)) args
     | Fix ((_,i),recd) ->
- 	extract_app env mle mlt (extract_fix env mle i recd) args 
+ 	extract_app env mle mlt (extract_fix env mle i recd) args
     | CoFix (i,recd) ->
  	extract_app env mle mlt (extract_fix env mle i recd) args
     | Cast (c,_,_) -> extract_term env mle mlt c args
-    | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false 
+    | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false
 
-(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) 
+(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
 
 and extract_maybe_term env mle mlt c =
-  try check_default env (type_of env c); 
-    extract_term env mle mlt c [] 
-  with NotDefault d -> 
+  try check_default env (type_of env c);
+    extract_term env mle mlt c []
+  with NotDefault d ->
     put_magic (mlt, Tdummy d) MLdummy
 
 (*s Generic way to deal with an application. *)
 
-(* We first type all arguments starting with unknown meta types. 
-   This gives us the expected type of the head. Then we use the 
+(* We first type all arguments starting with unknown meta types.
+   This gives us the expected type of the head. Then we use the
    [mk_head] to produce the ML head from this type. *)
 
-and extract_app env mle mlt mk_head args = 
-  let metas = List.map new_meta args in 
-  let type_head = type_recomp (metas, mlt) in 
-  let mlargs = List.map2 (extract_maybe_term env mle) metas args in 
+and extract_app env mle mlt mk_head args =
+  let metas = List.map new_meta args in
+  let type_head = type_recomp (metas, mlt) in
+  let mlargs = List.map2 (extract_maybe_term env mle) metas args in
   if mlargs = [] then mk_head type_head else MLapp (mk_head type_head, mlargs)
 
 (*s Auxiliary function used to extract arguments of constant or constructor. *)
 
-and make_mlargs env e s args typs = 
-  let l = ref s in 
+and make_mlargs env e s args typs =
+  let l = ref s in
   let keep () = match !l with [] -> true | b :: s -> l:=s; b=Keep in
-  let rec f = function  
-    | [], [] -> [] 
+  let rec f = function
+    | [], [] -> []
     | a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt))
     | _::la, _::lt -> f (la,lt)
-    | _ -> assert false 
+    | _ -> assert false
   in f (args,typs)
 
 (*s Extraction of a constant applied to arguments. *)
 
-and extract_cst_app env mle mlt kn args = 
-  (* First, the [ml_schema] of the constant, in expanded version. *) 
-  let nb,t = record_constant_type env kn None in 
-  let schema = nb, expand env t in 
+and extract_cst_app env mle mlt kn args =
+  (* First, the [ml_schema] of the constant, in expanded version. *)
+  let nb,t = record_constant_type env kn None in
+  let schema = nb, expand env t in
   (* Can we instantiate types variables for this constant ? *)
   (* In Ocaml, inside the definition of this constant, the answer is no. *)
-  let instantiated = 
+  let instantiated =
     if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
     else instantiation schema
-  in 
+  in
   (* Then the expected type of this constant. *)
-  let a = new_meta () in 
+  let a = new_meta () in
   (* We compare stored and expected types in two steps. *)
   (* First, can [kn] be applied to all args ? *)
-  let metas = List.map new_meta args in 
-  let magic1 = needs_magic (type_recomp (metas, a), instantiated) in 
+  let metas = List.map new_meta args in
+  let magic1 = needs_magic (type_recomp (metas, a), instantiated) in
   (* Second, is the resulting type compatible with the expected type [mlt] ? *)
-  let magic2 = needs_magic (a, mlt) in 
+  let magic2 = needs_magic (a, mlt) in
   (* The internal head receives a magic if [magic1] *)
-  let head = put_magic_if magic1 (MLglob (ConstRef kn)) in 
+  let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
   (* Now, the extraction of the arguments. *)
-  let s = type2signature env (snd schema) in 
-  let ls = List.length s in 
+  let s = type2signature env (snd schema) in
+  let ls = List.length s in
   let la = List.length args in
-  let mla = make_mlargs env mle s args metas in 
+  let mla = make_mlargs env mle s args metas in
   let mla =
-    if not magic1 then 
-      try 
-	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in 
+    if not magic1 then
+      try
+	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
 	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with _ -> mla
     else mla
-  in 			    
+  in 
   (* Different situations depending of the number of arguments: *)
   if ls = 0 then put_magic_if magic2 head
-  else if List.mem Keep s then 
-    if la >= ls || not (List.exists isKill s) 
-    then 
+  else if List.mem Keep s then
+    if la >= ls || not (List.exists isKill s)
+    then
       put_magic_if (magic2 && not magic1) (MLapp (head, mla))
-    else 
+    else
       (* Not enough arguments. We complete via eta-expansion. *)
       let ls' = ls-la in
       let s' = list_lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
       put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s')
-  else if List.mem (Kill Kother) s then 
+  else if List.mem (Kill Kother) s then
     (* In the special case of always false signature, one dummy lam is left. *)
-    (* So a [MLdummy] is left accordingly. *) 
-    if la >= ls 
+    (* So a [MLdummy] is left accordingly. *)
+    if la >= ls
     then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla))
     else put_magic_if magic2 (dummy_lams head (ls-la-1))
   else (* s is made only of [Kill Ktype] *)
-    if la >= ls 
+    if la >= ls
     then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
     else put_magic_if magic2 (dummy_lams head (ls-la))
 
@@ -648,7 +648,7 @@ and extract_cst_app env mle mlt kn args =
 (*s Extraction of an inductive constructor applied to arguments. *)
 
 (* \begin{itemize}
-   \item In ML, contructor arguments are uncurryfied. 
+   \item In ML, contructor arguments are uncurryfied.
    \item We managed to suppress logical parts inside inductive definitions,
    but they must appears outside (for partial applications for instance)
    \item We also suppressed all Coq parameters to the inductives, since
@@ -657,223 +657,223 @@ and extract_cst_app env mle mlt kn args =
 
 and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   (* First, we build the type of the constructor, stored in small pieces. *)
-  let mi = extract_ind env kn in 
-  let params_nb = mi.ind_nparams in 
-  let oi = mi.ind_packets.(i) in 
+  let mi = extract_ind env kn in
+  let params_nb = mi.ind_nparams in
+  let oi = mi.ind_packets.(i) in
   let nb_tvars = List.length oi.ip_vars
   and types = List.map (expand env) oi.ip_types.(j-1) in
-  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in 
+  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
-  let type_cons = instantiation (nb_tvars, type_cons) in 
+  let type_cons = instantiation (nb_tvars, type_cons) in
   (* Then, the usual variables [s], [ls], [la], ... *)
   let s = List.map (type2sign env) types in
-  let ls = List.length s in 
-  let la = List.length args in 
+  let ls = List.length s in
+  let la = List.length args in
   assert (la <= ls + params_nb);
-  let la' = max 0 (la - params_nb) in 
-  let args' = list_lastn la' args in 
+  let la' = max 0 (la - params_nb) in
+  let args' = list_lastn la' args in
   (* Now, we build the expected type of the constructor *)
-  let metas = List.map new_meta args' in 
+  let metas = List.map new_meta args' in
   (* If stored and expected types differ, then magic! *)
-  let a = new_meta () in 
+  let a = new_meta () in
   let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
-  let magic2 = needs_magic (a, mlt) in 
-  let head mla = 
-    if mi.ind_info = Singleton then 
+  let magic2 = needs_magic (a, mlt) in
+  let head mla =
+    if mi.ind_info = Singleton then
       put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
     else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
-  in 
+  in
   (* Different situations depending of the number of arguments: *)
-  if la < params_nb then 
-    let head' = head (eta_args_sign ls s) in 
-    put_magic_if magic2 
+  if la < params_nb then
+    let head' = head (eta_args_sign ls s) in
+    put_magic_if magic2
       (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
-  else 
-    let mla = make_mlargs env mle s args' metas in 
-    if la = ls + params_nb 
+  else
+    let mla = make_mlargs env mle s args' metas in
+    if la = ls + params_nb
     then put_magic_if (magic2 && not magic1) (head mla)
-    else (* [ params_nb <= la <= ls + params_nb ] *) 
-      let ls' = params_nb + ls - la in 
-      let s' = list_lastn ls' s in 
+    else (* [ params_nb <= la <= ls + params_nb ] *)
+      let ls' = params_nb + ls - la in
+      let s' = list_lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
       put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
 
 (*S Extraction of a case. *)
 
-and extract_case env mle ((kn,i) as ip,c,br) mlt = 
+and extract_case env mle ((kn,i) as ip,c,br) mlt =
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
   let ni = mis_constr_nargs_env env ip in
-  let br_size = Array.length br in 
-  assert (Array.length ni = br_size); 
+  let br_size = Array.length br in
+  assert (Array.length ni = br_size);
   if br_size = 0 then begin
     add_recursors env kn; (* May have passed unseen if logical ... *)
     MLexn "absurd case"
-  end else 
+  end else
     (* [c] has an inductive type, and is not a type scheme type. *)
-    let t = type_of env c in 
+    let t = type_of env c in
     (* The only non-informative case: [c] is of sort [Prop] *)
-    if (sort_of env t) = InProp then 
-      begin 
+    if (sort_of env t) = InProp then
+      begin
 	add_recursors env kn; (* May have passed unseen if logical ... *)
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
 	assert (br_size = 1);
 	let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
-	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in 
-	let e = extract_maybe_term env mle mlt br.(0) in 
+	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in
+	let e = extract_maybe_term env mle mlt br.(0) in
 	snd (case_expunge s e)
-      end 
-    else 
-      let mi = extract_ind env kn in 
-      let oi = mi.ind_packets.(i) in 
-      let metas = Array.init (List.length oi.ip_vars) new_meta in 
+      end
+    else
+      let mi = extract_ind env kn in
+      let oi = mi.ind_packets.(i) in
+      let metas = Array.init (List.length oi.ip_vars) new_meta in
       (* The extraction of the head. *)
       let type_head = Tglob (IndRef ip, Array.to_list metas) in
-      let a = extract_term env mle type_head c [] in 
+      let a = extract_term env mle type_head c [] in
       (* The extraction of each branch. *)
-      let extract_branch i = 
+      let extract_branch i =
 	(* The types of the arguments of the corresponding constructor. *)
-	let f t = type_subst_vect metas (expand env t) in 
+	let f t = type_subst_vect metas (expand env t) in
 	let l = List.map f oi.ip_types.(i) in
 	(* the corresponding signature *)
 	let s = List.map (type2sign env) oi.ip_types.(i) in
 	(* Extraction of the branch (in functional form). *)
-	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in 
+	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
 	(* We suppress dummy arguments according to signature. *)
 	let ids,e = case_expunge s e in
 	(ConstructRef (ip,i+1), List.rev ids, e)
       in
-      if mi.ind_info = Singleton then 
-	begin 
+      if mi.ind_info = Singleton then
+	begin
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
 	  assert (br_size = 1);
 	  let (_,ids,e') = extract_branch 0 in
 	  assert (List.length ids = 1);
 	  MLletin (List.hd ids,a,e')
-	end 
-      else 
+	end
+      else
 	(* Standard case: we apply [extract_branch]. *)
 	MLcase ((mi.ind_info,[]), a, Array.init br_size extract_branch)
-  
+
 (*s Extraction of a (co)-fixpoint. *)
 
-and extract_fix env mle i (fi,ti,ci as recd) mlt = 
-  let env = push_rec_types recd env in 
+and extract_fix env mle i (fi,ti,ci as recd) mlt =
+  let env = push_rec_types recd env in
   let metas = Array.map new_meta fi in
-  metas.(i) <- mlt; 
-  let mle = Array.fold_left Mlenv.push_type mle metas in 
-  let ei = array_map2 (extract_maybe_term env mle) metas ci in 
+  metas.(i) <- mlt;
+  let mle = Array.fold_left Mlenv.push_type mle metas in
+  let ei = array_map2 (extract_maybe_term env mle) metas ci in
   MLfix (i, Array.map id_of_name fi, ei)
 
 (*S ML declarations. *)
 
-(* [decomp_lams_eta env c t] finds the number [n] of products in the type [t], 
+(* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
-let rec decomp_lams_eta_n n env c t = 
-  let rels = fst (decomp_n_prod env none n t) in 
-  let rels = List.map (fun (id,_,c) -> (id,c)) rels in 
-  let m = nb_lam c in 
-  if m >= n then decompose_lam_n n c 
+let rec decomp_lams_eta_n n env c t =
+  let rels = fst (decomp_n_prod env none n t) in
+  let rels = List.map (fun (id,_,c) -> (id,c)) rels in
+  let m = nb_lam c in
+  if m >= n then decompose_lam_n n c
   else
-    let rels',c = decompose_lam c in 
-    let d = n - m in 
+    let rels',c = decompose_lam c in
+    let d = n - m in
     (* we'd better keep rels' as long as possible. *)
     let rels = (list_firstn d rels) @ rels' in
-    let eta_args = List.rev_map mkRel (interval 1 d) in 
+    let eta_args = List.rev_map mkRel (interval 1 d) in
     rels, applist (lift d c,eta_args)
 
 (*s From a constant to a ML declaration. *)
 
-let extract_std_constant env kn body typ = 
-  reset_meta_count (); 
+let extract_std_constant env kn body typ =
+  reset_meta_count ();
   (* The short type [t] (i.e. possibly with abbreviations). *)
-  let t = snd (record_constant_type env kn (Some typ)) in 
+  let t = snd (record_constant_type env kn (Some typ)) in
   (* The real type [t']: without head lambdas, expanded, *)
   (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
-  let l,t' = type_decomp (expand env (var2var' t)) in 
-  let s = List.map (type2sign env) l in 
+  let l,t' = type_decomp (expand env (var2var' t)) in
+  let s = List.map (type2sign env) l in
   (* The initial ML environment. *)
-  let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
+  let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
   (* Decomposing the top level lambdas of [body]. *)
   let rels,c = decomp_lams_eta_n (List.length s) env body typ in
   (* The lambdas names. *)
-  let ids = List.map (fun (n,_) -> id_of_name n) rels in 
+  let ids = List.map (fun (n,_) -> id_of_name n) rels in
   (* The according Coq environment. *)
   let env = push_rels_assum rels env in
   (* The real extraction: *)
   let e = extract_term env mle t' c [] in
-  (* Expunging term and type from dummy lambdas. *) 
+  (* Expunging term and type from dummy lambdas. *)
   term_expunge s (ids,e), type_expunge env t
 
-let extract_fixpoint env vkn (fi,ti,ci) = 
-  let n = Array.length vkn in 
+let extract_fixpoint env vkn (fi,ti,ci) =
+  let n = Array.length vkn in
   let types = Array.make n (Tdummy Kother)
-  and terms = Array.make n MLdummy in 
-  let kns = Array.to_list vkn in 
-  current_fixpoints := kns; 
+  and terms = Array.make n MLdummy in
+  let kns = Array.to_list vkn in
+  current_fixpoints := kns;
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
-  let sub = List.rev_map mkConst kns in 
-  for i = 0 to n-1 do 
-    if sort_of env ti.(i) <> InProp then begin 
+  let sub = List.rev_map mkConst kns in
+  for i = 0 to n-1 do
+    if sort_of env ti.(i) <> InProp then begin
       let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
-      terms.(i) <- e; 
+      terms.(i) <- e;
       types.(i) <- t;
-    end 
-  done; 
+    end
+  done;
   current_fixpoints := [];
-  Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) 
-		 
-let extract_constant env kn cb = 
-  let r = ConstRef kn in 
-  let typ = Typeops.type_of_constant_type env cb.const_type in 
+  Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
+
+let extract_constant env kn cb =
+  let r = ConstRef kn in
+  let typ = Typeops.type_of_constant_type env cb.const_type in
   match cb.const_body with
-    | None -> (* A logical axiom is risky, an informative one is fatal. *) 
+    | None -> (* A logical axiom is risky, an informative one is fatal. *)
         (match flag_of_type env typ with
-	   | (Info,TypeScheme) -> 
-	       if not (is_custom r) then add_info_axiom r; 
-	       let n = type_scheme_nb_args env typ in 
-	       let ids = iterate (fun l -> anonymous::l) n [] in 
-	       Dtype (r, ids, Taxiom) 
-           | (Info,Default) -> 
-	       if not (is_custom r) then add_info_axiom r; 
-	       let t = snd (record_constant_type env kn (Some typ)) in 
-	       Dterm (r, MLaxiom, type_expunge env t) 
-           | (Logic,TypeScheme) -> 
+	   | (Info,TypeScheme) ->
+	       if not (is_custom r) then add_info_axiom r;
+	       let n = type_scheme_nb_args env typ in
+	       let ids = iterate (fun l -> anonymous::l) n [] in
+	       Dtype (r, ids, Taxiom)
+           | (Info,Default) ->
+	       if not (is_custom r) then add_info_axiom r;
+	       let t = snd (record_constant_type env kn (Some typ)) in
+	       Dterm (r, MLaxiom, type_expunge env t)
+           | (Logic,TypeScheme) ->
 	       add_log_axiom r; Dtype (r, [], Tdummy Ktype)
-	   | (Logic,Default) -> 
+	   | (Logic,Default) ->
 	       add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother))
     | Some body ->
 	(match flag_of_type env typ with
 	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
 	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype)
-	   | (Info, Default) -> 
-	       let e,t = extract_std_constant env kn (force body) typ in 
+	   | (Info, Default) ->
+	       let e,t = extract_std_constant env kn (force body) typ in
 	       Dterm (r,e,t)
-	   | (Info, TypeScheme) -> 
-	       let s,vl = type_sign_vl env typ in 
-               let db = db_from_sign s in 
-               let t = extract_type_scheme env db (force body) (List.length s) 
+	   | (Info, TypeScheme) ->
+	       let s,vl = type_sign_vl env typ in
+               let db = db_from_sign s in
+               let t = extract_type_scheme env db (force body) (List.length s)
 	       in Dtype (r, vl, t))
 
-let extract_constant_spec env kn cb = 
-  let r = ConstRef kn in 
-  let typ = Typeops.type_of_constant_type env cb.const_type in 
-  match flag_of_type env typ with 
+let extract_constant_spec env kn cb =
+  let r = ConstRef kn in
+  let typ = Typeops.type_of_constant_type env cb.const_type in
+  match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
-    | (Logic, Default) -> Sval (r, Tdummy Kother) 
-    | (Info, TypeScheme) -> 
-	let s,vl = type_sign_vl env typ in 
-	(match cb.const_body with 
+    | (Logic, Default) -> Sval (r, Tdummy Kother)
+    | (Info, TypeScheme) ->
+	let s,vl = type_sign_vl env typ in
+	(match cb.const_body with
 	  | None -> Stype (r, vl, None)
-	  | Some body -> 
-	      let db = db_from_sign s in 
+	  | Some body ->
+	      let db = db_from_sign s in
 	      let t = extract_type_scheme env db (force body) (List.length s)
-	      in Stype (r, vl, Some t)) 
-    | (Info, Default) -> 
-	let t = snd (record_constant_type env kn (Some typ)) in 
+	      in Stype (r, vl, Some t))
+    | (Info, Default) ->
+	let t = snd (record_constant_type env kn (Some typ)) in
 	Sval (r, type_expunge env t)
 
 let extract_with_type env cb =
@@ -887,30 +887,30 @@ let extract_with_type env cb =
 	Some (vl, t)
     | _ -> None
 
-		   
-let extract_inductive env kn = 
-  let ind = extract_ind env kn in 
-  add_recursors env kn; 
-  let f l = List.filter (fun t -> not (isDummy (expand env t))) l in 
-  let packets = 
-    Array.map (fun p -> { p with ip_types = Array.map f p.ip_types }) 
+
+let extract_inductive env kn =
+  let ind = extract_ind env kn in
+  add_recursors env kn;
+  let f l = List.filter (fun t -> not (isDummy (expand env t))) l in
+  let packets =
+    Array.map (fun p -> { p with ip_types = Array.map f p.ip_types })
       ind.ind_packets
   in { ind with ind_packets = packets }
 
-(*s Is a [ml_decl] logical ? *) 
+(*s Is a [ml_decl] logical ? *)
 
-let logical_decl = function 
+let logical_decl = function
   | Dterm (_,MLdummy,Tdummy _) -> true
-  | Dtype (_,[],Tdummy _) -> true 
-  | Dfix (_,av,tv) -> 
-      (array_for_all ((=) MLdummy) av) && 
+  | Dtype (_,[],Tdummy _) -> true
+  | Dfix (_,av,tv) ->
+      (array_for_all ((=) MLdummy) av) &&
       (array_for_all isDummy tv)
   | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
 (*s Is a [ml_spec] logical ? *)
 
-let logical_spec = function 
+let logical_spec = function
   | Stype (_, [], Some (Tdummy _)) -> true
   | Sval (_,Tdummy _) -> true
   | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 343d2b69a..2c534ea7b 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -23,12 +23,12 @@ val extract_constant_spec : env -> constant -> constant_body -> ml_spec
 
 val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option
 
-val extract_fixpoint : 
-  env -> constant array -> (constr, types) prec_declaration -> ml_decl 
+val extract_fixpoint :
+  env -> constant array -> (constr, types) prec_declaration -> ml_decl
 
 val extract_inductive : env -> kernel_name -> ml_ind
 
-(*s Is a [ml_decl] or a [ml_spec] logical ? *) 
+(*s Is a [ml_decl] or a [ml_spec] logical ? *)
 
 val logical_decl : ml_decl -> bool
 val logical_spec : ml_spec -> bool
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index cb95808d6..193805b98 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -41,7 +41,7 @@ VERNAC COMMAND EXTEND Extraction
 | [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ]
 
 (* Monolithic extraction to a file *)
-| [ "Extraction" string(f) ne_global_list(l) ] 
+| [ "Extraction" string(f) ne_global_list(l) ]
   -> [ full_extraction (Some f) l ]
 END
 
@@ -58,18 +58,18 @@ END
 
 (* Target Language *)
 VERNAC COMMAND EXTEND ExtractionLanguage
-| [ "Extraction" "Language" language(l) ] 
+| [ "Extraction" "Language" language(l) ]
   -> [ extraction_language l ]
 END
 
 VERNAC COMMAND EXTEND ExtractionInline
 (* Custom inlining directives *)
-| [ "Extraction" "Inline" ne_global_list(l) ] 
+| [ "Extraction" "Inline" ne_global_list(l) ]
   -> [ extraction_inline true l ]
 END
 
 VERNAC COMMAND EXTEND ExtractionNoInline
-| [ "Extraction" "NoInline" ne_global_list(l) ] 
+| [ "Extraction" "NoInline" ne_global_list(l) ]
   -> [ extraction_inline false l ]
 END
 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 8cf84cc5b..6403e7bbe 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -25,27 +25,27 @@ open Common
 let pr_lower_id id = str (String.uncapitalize (string_of_id id))
 let pr_upper_id id = str (String.capitalize (string_of_id id))
 
-let keywords =     
+let keywords =
   List.fold_right (fun s -> Idset.add (id_of_string s))
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
-    "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
+    "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
   Idset.empty
 
 let preamble mod_name used_modules usf =
   let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
-  in 
-  (if not usf.magic then mt () 
+  in
+  (if not usf.magic then mt ()
    else
      str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
      str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
   ++
   str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
   str "import qualified Prelude" ++ fnl () ++
-  prlist pp_import used_modules ++ fnl () ++ 
+  prlist pp_import used_modules ++ fnl () ++
   (if used_modules = [] then mt () else fnl ()) ++
-  (if not usf.magic then mt () 
+  (if not usf.magic then mt ()
    else str "\
 #ifdef __GLASGOW_HASKELL__
 import qualified GHC.Base
@@ -56,7 +56,7 @@ import qualified IOExts
 unsafeCoerce = IOExts.unsafeCoerce
 #endif" ++ fnl2 ())
   ++
-  (if not usf.mldummy then mt () 
+  (if not usf.mldummy then mt ()
    else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
 
 let pp_abst = function
@@ -67,36 +67,36 @@ let pp_abst = function
 
 (*s The pretty-printer for haskell syntax *)
 
-let pp_global k r = 
-  if is_inline_custom r then str (find_custom r) 
+let pp_global k r =
+  if is_inline_custom r then str (find_custom r)
   else str (Common.pp_global k r)
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let kn_sig = 
-  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in 
+let kn_sig =
+  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
   make_kn specif empty_dirpath (mk_label "sig")
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
-    | Tmeta _ | Tvar' _ -> assert false 
+    | Tmeta _ | Tvar' _ -> assert false
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
-    | Tglob (r,[]) -> pp_global Type r	
-    | Tglob (r,l) -> 
-	if r = IndRef (kn_sig,0) then 
+    | Tglob (r,[]) -> pp_global Type r
+    | Tglob (r,l) ->
+	if r = IndRef (kn_sig,0) then
 	  pp_type true vl (List.hd l)
-	else 
-	  pp_par par 
-	    (pp_global Type r ++ spc () ++ 
+	else
+	  pp_par par
+	    (pp_global Type r ++ spc () ++
 	     prlist_with_sep spc (pp_type true vl) l)
     | Tarr (t1,t2) ->
-	pp_par par 
+	pp_par par
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy _ -> str "()"
     | Tunknown -> str "()"
     | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
- in 
+ in
   hov 0 (pp_rec par t)
 
 (*s Pretty-printing of expressions. [par] indicates whether
@@ -107,19 +107,19 @@ let rec pp_type par vl t =
 let expr_needs_par = function
   | MLlam _  -> true
   | MLcase _ -> true
-  | _        -> false 
+  | _        -> false
 
 
 let rec pp_expr par env args =
   let par' = args <> [] || par
-  and apply st = pp_apply st par args in 
+  and apply st = pp_apply st par args in
   function
-    | MLrel n -> 
+    | MLrel n ->
 	let id = get_db_name n env in apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
-    | MLlam _ as a -> 
+    | MLlam _ as a ->
       	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
 	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
@@ -129,15 +129,15 @@ let rec pp_expr par env args =
 	let pp_id = pr_id (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
-	hv 0 
-	  (apply 
-	     (pp_par par' 
-		(hv 0 
-		   (hov 5 
-		      (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ 
+	hv 0
+	  (apply
+	     (pp_par par'
+		(hv 0
+		   (hov 5
+		      (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++
 		    spc () ++ str "in") ++
 		 spc () ++ hov 0 pp_a2)))
-    | MLglob r -> 
+    | MLglob r ->
 	apply (pp_global Term r)
     | MLcons (_,r,[]) ->
 	assert (args=[]); pp_global Cons r
@@ -146,47 +146,47 @@ let rec pp_expr par env args =
 	pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
     | MLcons (_,r,args') ->
 	assert (args=[]);
-	pp_par par (pp_global Cons r ++ spc () ++ 
+	pp_par par (pp_global Cons r ++ spc () ++
 		    prlist_with_sep spc (pp_expr true env []) args')
     | MLcase ((_,factors),t, pv) ->
-      	apply (pp_par par' 
+      	apply (pp_par par'
 		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
 		       fnl () ++ str "  " ++ pp_pat env factors pv)))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
-    | MLexn s -> 
+    | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLmagic a ->  
+    | MLmagic a ->
 	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
 
-and pp_pat env factors pv = 
+and pp_pat env factors pv =
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev ids) env in
     let par = expr_needs_par t in
     hov 2 (pp_global Cons name ++
-	   (match ids with 
+	   (match ids with
 	      | [] -> mt ()
-	      | _  -> (str " " ++ 
-		       prlist_with_sep 
+	      | _  -> (str " " ++
+		       prlist_with_sep
 			 (fun () -> (spc ())) pr_id (List.rev ids))) ++
 	   str " ->" ++ spc () ++ pp_expr par env' [] t)
-  in 
-  prvecti 
-    (fun i x -> if List.mem i factors then mt () else 
+  in
+  prvecti
+    (fun i x -> if List.mem i factors then mt () else
        (pp_one_pat pv.(i) ++
 	if factors = [] && i = Array.length pv - 1 then mt ()
 	else fnl () ++ str "  ")) pv
   ++
-  match factors with 
+  match factors with
     | [] -> mt ()
-    | i::_ -> 
-	let (_,ids,t) = pv.(i) in 
-	let t = ast_lift (-List.length ids) t in 
+    | i::_ ->
+	let (_,ids,t) = pv.(i) in
+	let t = ast_lift (-List.length ids) t in
 	hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t)
 
 (*s names of the functions ([ids]) are already pushed in [env],
@@ -194,12 +194,12 @@ and pp_pat env factors pv =
 
 and pp_fix par env i (ids,bl) args =
   pp_par par
-    (v 0  
+    (v 0
        (v 2 (str "let" ++ fnl () ++
-	     prvect_with_sep fnl 
-	       (fun (fi,ti) -> pp_function env (pr_id fi) ti) 
-	       (array_map2 (fun a b -> a,b) ids bl)) ++ 
-	fnl () ++ 
+	     prvect_with_sep fnl
+	       (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	       (array_map2 (fun a b -> a,b) ids bl)) ++
+	fnl () ++
 	hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 
 and pp_function env f t =
@@ -213,19 +213,19 @@ and pp_function env f t =
 
 let pp_comment s = str "-- " ++ s ++ fnl ()
 
-let pp_logical_ind packet = 
+let pp_logical_ind packet =
   pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
-  pp_comment (str "with constructors : " ++ 
+  pp_comment (str "with constructors : " ++
 	      prvect_with_sep spc pr_id packet.ip_consnames)
 
-let pp_singleton kn packet = 
-  let l = rename_tvars keywords packet.ip_vars in 
-  let l' = List.rev l in 
-  hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ 
+let pp_singleton kn packet =
+  let l = rename_tvars keywords packet.ip_vars in
+  let l' = List.rev l in
+  hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++
 	 prlist_with_sep spc pr_id l ++
 	 (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
 	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment (str "singleton inductive, whose constructor was " ++ 
+	 pp_comment (str "singleton inductive, whose constructor was " ++
 		     pr_id packet.ip_consnames.(0)))
 
 let pp_one_ind ip pl cv =
@@ -233,102 +233,102 @@ let pp_one_ind ip pl cv =
   let pp_constructor (r,l) =
     (pp_global Cons r ++
      match l with
-       | [] -> (mt ()) 
+       | [] -> (mt ())
        | _  -> (str " " ++
-      	       	prlist_with_sep 
+      	       	prlist_with_sep
 		  (fun () -> (str " ")) (pp_type true pl) l))
   in
-  str (if Array.length cv = 0 then "type " else "data ") ++ 
+  str (if Array.length cv = 0 then "type " else "data ") ++
   pp_global Type (IndRef ip) ++ str " " ++
   prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
   (if pl = [] then mt () else str " ") ++
   if Array.length cv = 0 then str "= () -- empty inductive"
-  else 
+  else
     (v 0 (str "= " ++
-	  prvect_with_sep (fun () -> fnl () ++ str "  | ") pp_constructor 
+	  prvect_with_sep (fun () -> fnl () ++ str "  | ") pp_constructor
 	    (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
-  
+
 let rec pp_ind first kn i ind =
-  if i >= Array.length ind.ind_packets then 
-    if first then mt () else fnl () 
-  else 
-    let ip = (kn,i) in 
-    let p = ind.ind_packets.(i) in 
-    if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind 
-    else 
-      if p.ip_logical then  
+  if i >= Array.length ind.ind_packets then
+    if first then mt () else fnl ()
+  else
+    let ip = (kn,i) in
+    let p = ind.ind_packets.(i) in
+    if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind
+    else
+      if p.ip_logical then
 	pp_logical_ind p ++ pp_ind first kn (i+1) ind
-      else 
-	pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ 
+      else
+	pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++
 	pp_ind false kn (i+1) ind
-	  
+
 
 (*s Pretty-printing of a declaration. *)
 
 let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
 
 let pp_decl = function
-  | Dind (kn,i) when i.ind_info = Singleton -> 
+  | Dind (kn,i) when i.ind_info = Singleton ->
       pp_singleton kn i.ind_packets.(0) ++ fnl ()
   | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
   | Dtype (r, l, t) ->
-      if is_inline_custom r then mt () 
-      else 
-	let l = rename_tvars keywords l in 
-	let st = 
-	  try 
-	    let ids,s = find_type_custom r in 
+      if is_inline_custom r then mt ()
+      else
+	let l = rename_tvars keywords l in
+	let st =
+	  try
+	    let ids,s = find_type_custom r in
 	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
-	  with not_found -> 
+	  with not_found ->
 	    prlist (fun id -> pr_id id ++ str " ") l ++
 	    if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
 	    else str "=" ++ spc () ++ pp_type false l t
-	in 
+	in
 	hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
   | Dfix (rv, defs, typs) ->
-      let max = Array.length rv in 
-      let rec iter i = 
-	if i = max then mt () 
+      let max = Array.length rv in
+      let rec iter i =
+	if i = max then mt ()
 	else
-	  let e = pp_global Term rv.(i) in 
-	  e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () 
+	  let e = pp_global Term rv.(i) in
+	  e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl ()
 	  ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 ()
 	  ++ iter (i+1)
       in iter 0
   | Dterm (r, a, t) ->
-      if is_inline_custom r then mt () 
-      else 
-	let e = pp_global Term r in 
+      if is_inline_custom r then mt ()
+      else
+	let e = pp_global Term r in
 	e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
-	  if is_custom r then 	
+	  if is_custom r then 
 	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
-	  else 
+	  else
 	    hov 0 (pp_function (empty_env ()) e a ++ fnl2 ())
 
-let pp_structure_elem = function 
+let pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d
-  | (l,SEmodule m) -> 
+  | (l,SEmodule m) ->
       failwith "TODO: Haskell extraction of modules not implemented yet"
-  | (l,SEmodtype m) -> 
+  | (l,SEmodtype m) ->
       failwith "TODO: Haskell extraction of modules not implemented yet"
 
-let pp_struct = 
-  let pp_sel (mp,sel) = 
-    push_visible mp None; 
-    let p = prlist_strict pp_structure_elem sel in 
+let pp_struct =
+  let pp_sel (mp,sel) =
+    push_visible mp None;
+    let p = prlist_strict pp_structure_elem sel in
     pop_visible (); p
-  in 
-  prlist_strict pp_sel 
+  in
+  prlist_strict pp_sel
 
 
 let haskell_descr = {
-  keywords = keywords;  
-  file_suffix = ".hs"; 
-  capital_file = true;  
-  preamble = preamble; 
-  pp_struct = pp_struct; 
+  keywords = keywords;
+  file_suffix = ".hs";
+  capital_file = true;
+  preamble = preamble;
+  pp_struct = pp_struct;
   sig_suffix = None;
-  sig_preamble = (fun _ _ _ -> mt ()); 
+  sig_preamble = (fun _ _ _ -> mt ());
   pp_sig = (fun _ -> mt ());
-  pp_decl = pp_decl; 
+  pp_decl = pp_decl;
 }
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 3add72d8b..12ca9ad75 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -26,16 +26,16 @@ type kill_reason = Ktype | Kother
 
 type sign = Keep | Kill of kill_reason
 
-   
+
 (* Convention: outmost lambda/product gives the head of the list. *)
 
 type signature = sign list
 
 (*s ML type expressions. *)
 
-type ml_type = 
+type ml_type =
   | Tarr    of ml_type * ml_type
-  | Tglob   of global_reference * ml_type list 
+  | Tglob   of global_reference * ml_type list
   | Tvar    of int
   | Tvar'   of int (* same as Tvar, used to avoid clash *)
   | Tmeta   of ml_meta (* used during ML type reconstruction *)
@@ -45,61 +45,61 @@ type ml_type =
 
 and ml_meta = { id : int; mutable contents : ml_type option }
 
-(* ML type schema. 
+(* ML type schema.
    The integer is the number of variable in the schema. *)
 
-type ml_schema = int * ml_type 
+type ml_schema = int * ml_type
 
 (*s ML inductive types. *)
 
-type inductive_info = 
-  | Singleton 
-  | Coinductive 
-  | Standard 
-  | Record of global_reference list 
+type inductive_info =
+  | Singleton
+  | Coinductive
+  | Standard
+  | Record of global_reference list
 
 type case_info = int list (* list of branches to merge in a _ pattern *)
 
-(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. 
+(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
    If the inductive is logical ([ip_logical = false]), then all other fields
-   are unused. Otherwise, 
-   [ip_sign] is a signature concerning the arguments of the inductive, 
-   [ip_vars] contains the names of the type variables surviving in ML, 
-   [ip_types] contains the ML types of all constructors.    
+   are unused. Otherwise,
+   [ip_sign] is a signature concerning the arguments of the inductive,
+   [ip_vars] contains the names of the type variables surviving in ML,
+   [ip_types] contains the ML types of all constructors.
 *)
 
-type ml_ind_packet = { 
-  ip_typename : identifier; 
-  ip_consnames : identifier array; 
+type ml_ind_packet = {
+  ip_typename : identifier;
+  ip_consnames : identifier array;
   ip_logical : bool;
-  ip_sign : signature; 
-  ip_vars : identifier list; 
-  ip_types : (ml_type list) array }  
+  ip_sign : signature;
+  ip_vars : identifier list;
+  ip_types : (ml_type list) array }
 
 (* [ip_nparams] contains the number of parameters. *)
 
-type equiv = 
+type equiv =
   | NoEquiv
-  | Equiv of kernel_name 
+  | Equiv of kernel_name
   | RenEquiv of string
 
 type ml_ind = {
   ind_info : inductive_info;
-  ind_nparams : int; 	       
+  ind_nparams : int; 
   ind_packets : ml_ind_packet array;
   ind_equiv : equiv
 }
 
 (*s ML terms. *)
 
-type ml_ast = 
+type ml_ast =
   | MLrel    of int
   | MLapp    of ml_ast * ml_ast list
   | MLlam    of identifier * ml_ast
   | MLletin  of identifier * ml_ast * ml_ast
   | MLglob   of global_reference
   | MLcons   of inductive_info * global_reference * ml_ast list
-  | MLcase   of (inductive_info*case_info) * ml_ast * 
+  | MLcase   of (inductive_info*case_info) * ml_ast *
       (global_reference * identifier list * ml_ast) array
   | MLfix    of int * identifier array * ml_ast array
   | MLexn    of string
@@ -109,52 +109,52 @@ type ml_ast =
 
 (*s ML declarations. *)
 
-type ml_decl = 
+type ml_decl =
   | Dind  of kernel_name * ml_ind
   | Dtype of global_reference * identifier list * ml_type
   | Dterm of global_reference * ml_ast * ml_type
   | Dfix  of global_reference array * ml_ast array * ml_type array
 
-type ml_spec = 
+type ml_spec =
   | Sind  of kernel_name * ml_ind
-  | Stype of global_reference * identifier list * ml_type option 
+  | Stype of global_reference * identifier list * ml_type option
   | Sval  of global_reference * ml_type
 
-type ml_specif = 
-  | Spec of ml_spec 
+type ml_specif =
+  | Spec of ml_spec
   | Smodule of ml_module_type
   | Smodtype of ml_module_type
 
-and ml_module_type = 
+and ml_module_type =
   | MTident of module_path
   | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
   | MTsig of mod_self_id * ml_module_sig
   | MTwith of ml_module_type * ml_with_declaration
 
-and ml_with_declaration =  
+and ml_with_declaration =
   | ML_With_type of identifier list * identifier list * ml_type
   | ML_With_module of identifier list * module_path
 
 and ml_module_sig = (label * ml_specif) list
 
-type ml_structure_elem = 
+type ml_structure_elem =
   | SEdecl of ml_decl
   | SEmodule of ml_module
   | SEmodtype of ml_module_type
 
 and ml_module_expr =
   | MEident of module_path
-  | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr 
+  | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr
   | MEstruct of mod_self_id * ml_module_structure
   | MEapply of ml_module_expr * ml_module_expr
 
 and ml_module_structure = (label * ml_structure_elem) list
 
-and ml_module = 
-    { ml_mod_expr : ml_module_expr; 
+and ml_module =
+    { ml_mod_expr : ml_module_expr;
       ml_mod_type : ml_module_type }
 
-(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp] 
+(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp]
    implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
 
 type ml_structure = (module_path * ml_module_structure) list
@@ -162,27 +162,27 @@ type ml_structure = (module_path * ml_module_structure) list
 type ml_signature = (module_path * ml_module_sig) list
 
 type unsafe_needs = {
-  mldummy : bool; 
-  tdummy : bool; 
-  tunknown : bool; 
+  mldummy : bool;
+  tdummy : bool;
+  tunknown : bool;
   magic : bool
 }
 
 type language_descr = {
-  keywords : Idset.t; 
+  keywords : Idset.t;
 
   (* Concerning the source file *)
-  file_suffix : string;  
+  file_suffix : string;
   capital_file : bool; (* should we capitalize filenames ? *)
-  preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; 
-  pp_struct : ml_structure -> std_ppcmds; 
+  preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+  pp_struct : ml_structure -> std_ppcmds;
 
   (* Concerning a possible interface file *)
-  sig_suffix : string option; 
+  sig_suffix : string option;
   sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
-  pp_sig : ml_signature -> std_ppcmds; 
+  pp_sig : ml_signature -> std_ppcmds;
 
   (* for an isolated declaration print *)
-  pp_decl : ml_decl -> std_ppcmds; 
+  pp_decl : ml_decl -> std_ppcmds;
 
-}  
+}
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 06185875f..213df31e6 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -31,34 +31,34 @@ let dummy_name = id_of_string "_"
 let id_of_name = function
   | Anonymous -> anonymous
   | Name id when id = dummy_name -> anonymous
-  | Name id -> id 
+  | Name id -> id
 
 (*S Operations upon ML types (with meta). *)
 
-let meta_count = ref 0 
-		     
+let meta_count = ref 0
+
 let reset_meta_count () = meta_count := 0
-			      
-let new_meta _ = 
-  incr meta_count; 
+
+let new_meta _ =
+  incr meta_count;
   Tmeta {id = !meta_count; contents = None}
 
 (*s Sustitution of [Tvar i] by [t] in a ML type. *)
 
-let type_subst i t0 t = 
+let type_subst i t0 t =
   let rec subst t = match t with
     | Tvar j when i = j -> t0
-    | Tmeta {contents=None} -> t 
+    | Tmeta {contents=None} -> t
     | Tmeta {contents=Some u} -> subst u
     | Tarr (a,b) -> Tarr (subst a, subst b)
     | Tglob (r, l) -> Tglob (r, List.map subst l)
-    | a -> a 
+    | a -> a
   in subst t
-       
+
 (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
 
-let type_subst_list l t = 
-  let rec subst t = match t with 
+let type_subst_list l t =
+  let rec subst t = match t with
     | Tvar j -> List.nth l (j-1)
     | Tmeta {contents=None} -> t
     | Tmeta {contents=Some u} -> subst u
@@ -69,8 +69,8 @@ let type_subst_list l t =
 
 (* Simultaneous substitution of [[|Tvar 1; ... ; Tvar n|]] by [v] in a ML type. *)
 
-let type_subst_vect v t = 
-  let rec subst t = match t with 
+let type_subst_vect v t =
+  let rec subst t = match t with
     | Tvar j -> v.(j-1)
     | Tmeta {contents=None} -> t
     | Tmeta {contents=Some u} -> subst u
@@ -90,17 +90,17 @@ let rec type_occurs alpha t =
   | Tmeta {id=beta; contents=None} -> alpha = beta
   | Tmeta {contents=Some u} -> type_occurs alpha u
   | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
-  | Tglob (r,l) -> List.exists (type_occurs alpha) l  
+  | Tglob (r,l) -> List.exists (type_occurs alpha) l
   | _ -> false
 
 (*s Most General Unificator *)
 
 let rec mgu = function
   | Tmeta m, Tmeta m' when m.id = m'.id -> ()
-  | Tmeta m, t when m.contents=None -> 
+  | Tmeta m, t when m.contents=None ->
       if type_occurs m.id t then raise Impossible
       else m.contents <- Some t
-  | t, Tmeta m when m.contents=None -> 
+  | t, Tmeta m when m.contents=None ->
       if type_occurs m.id t then raise Impossible
       else m.contents <- Some t
   | Tmeta {contents=Some u}, t -> mgu (u, t)
@@ -124,12 +124,12 @@ let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
 
 (*S ML type env. *)
 
-module Mlenv = struct 
-  
-  let meta_cmp m m' = compare m.id m'.id 
+module Mlenv = struct
+
+  let meta_cmp m m' = compare m.id m'.id
   module Metaset = Set.Make(struct type t = ml_meta let compare = meta_cmp end)
 
-  (* Main MLenv type. [env] is the real environment, whereas [free] 
+  (* Main MLenv type. [env] is the real environment, whereas [free]
      (tries to) record the free meta variables occurring in [env]. *)
 
   type t = { env : ml_schema list; mutable free : Metaset.t}
@@ -138,68 +138,68 @@ module Mlenv = struct
 
   let empty = { env = []; free = Metaset.empty }
 
-  (* [get] returns a instantiated copy of the n-th most recently added 
+  (* [get] returns a instantiated copy of the n-th most recently added
      type in the environment. *)
 
-  let get mle n = 
-    assert (List.length mle.env >= n); 
+  let get mle n =
+    assert (List.length mle.env >= n);
     instantiation (List.nth mle.env (n-1))
 
-  (* [find_free] finds the free meta in a type. *) 
+  (* [find_free] finds the free meta in a type. *)
 
-  let rec find_free set = function 
+  let rec find_free set = function
     | Tmeta m when m.contents = None -> Metaset.add m set
     | Tmeta {contents = Some t} -> find_free set t
     | Tarr (a,b) -> find_free (find_free set a) b
     | Tglob (_,l) -> List.fold_left find_free set l
     | _ -> set
 
-  (* The [free] set of an environment can be outdate after 
-     some unifications. [clean_free] takes care of that. *) 
-			
-  let clean_free mle = 
-    let rem = ref Metaset.empty 
-    and add = ref Metaset.empty in 
-    let clean m = match m.contents with 
-      | None -> () 
+  (* The [free] set of an environment can be outdate after
+     some unifications. [clean_free] takes care of that. *)
+
+  let clean_free mle =
+    let rem = ref Metaset.empty
+    and add = ref Metaset.empty in
+    let clean m = match m.contents with
+      | None -> ()
       | Some u -> rem := Metaset.add m !rem; add := find_free !add u
-    in 
-    Metaset.iter clean mle.free; 
+    in
+    Metaset.iter clean mle.free;
     mle.free <- Metaset.union (Metaset.diff mle.free !rem) !add
 
   (* From a type to a type schema. If a [Tmeta] is still uninstantiated
      and does appears in the [mle], then it becomes a [Tvar]. *)
 
-  let generalization mle t = 
-    let c = ref 0 in 
-    let map = ref (Intmap.empty : int Intmap.t) in 
-    let add_new i = incr c; map := Intmap.add i !c !map; !c in 
-    let rec meta2var t = match t with 
-      | Tmeta {contents=Some u} -> meta2var u 
-      | Tmeta ({id=i} as m) -> 
-	  (try Tvar (Intmap.find i !map) 
-	   with Not_found ->  
-	     if Metaset.mem m mle.free then t 
+  let generalization mle t =
+    let c = ref 0 in
+    let map = ref (Intmap.empty : int Intmap.t) in
+    let add_new i = incr c; map := Intmap.add i !c !map; !c in
+    let rec meta2var t = match t with
+      | Tmeta {contents=Some u} -> meta2var u
+      | Tmeta ({id=i} as m) ->
+	  (try Tvar (Intmap.find i !map)
+	   with Not_found ->
+	     if Metaset.mem m mle.free then t
 	     else Tvar (add_new i))
       | Tarr (t1,t2) -> Tarr (meta2var t1, meta2var t2)
-      | Tglob (r,l) -> Tglob (r, List.map meta2var l) 
-      | t -> t 
+      | Tglob (r,l) -> Tglob (r, List.map meta2var l)
+      | t -> t
     in !c, meta2var t
-	
+
   (* Adding a type in an environment, after generalizing. *)
 
-  let push_gen mle t = 
-    clean_free mle; 
+  let push_gen mle t =
+    clean_free mle;
     { env = generalization mle t :: mle.env; free = mle.free }
 
   (* Adding a type with no [Tvar], hence no generalization needed. *)
 
-  let push_type {env=e;free=f} t = 
-    { env = (0,t) :: e; free = find_free f t} 
-    
+  let push_type {env=e;free=f} t =
+    { env = (0,t) :: e; free = find_free f t}
+
   (* Adding a type with no [Tvar] nor [Tmeta]. *)
 
-  let push_std_type {env=e;free=f} t = 
+  let push_std_type {env=e;free=f} t =
     { env = (0,t) :: e; free = f}
 
 end
@@ -208,7 +208,7 @@ end
 
 (*s Does a section path occur in a ML type ? *)
 
-let rec type_mem_kn kn = function 
+let rec type_mem_kn kn = function
   | Tmeta {contents = Some t} -> type_mem_kn kn t
   | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l
   | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b)
@@ -216,31 +216,31 @@ let rec type_mem_kn kn = function
 
 (*s Greatest variable occurring in [t]. *)
 
-let type_maxvar t = 
-  let rec parse n = function 
+let type_maxvar t =
+  let rec parse n = function
     | Tmeta {contents = Some t} -> parse n t
-    | Tvar i -> max i n 
+    | Tvar i -> max i n
     | Tarr (a,b) -> parse (parse n a) b
-    | Tglob (_,l) -> List.fold_left parse n l 
-    | _ -> n 
+    | Tglob (_,l) -> List.fold_left parse n l
+    | _ -> n
   in parse 0 t
 
-(*s From [a -> b -> c] to [[a;b],c]. *) 
+(*s From [a -> b -> c] to [[a;b],c]. *)
 
-let rec type_decomp = function 
-  | Tmeta {contents = Some t} -> type_decomp t 
-  | Tarr (a,b) -> let l,h = type_decomp b in a::l, h 
+let rec type_decomp = function
+  | Tmeta {contents = Some t} -> type_decomp t
+  | Tarr (a,b) -> let l,h = type_decomp b in a::l, h
   | a -> [],a
 
 (*s The converse: From [[a;b],c] to [a -> b -> c]. *)
 
-let rec type_recomp (l,t) = match l with 
-  | [] -> t 
+let rec type_recomp (l,t) = match l with
+  | [] -> t
   | a::l -> Tarr (a, type_recomp (l,t))
 
 (*s Translating [Tvar] to [Tvar'] to avoid clash. *)
 
-let rec var2var' = function 
+let rec var2var' = function
   | Tmeta {contents = Some t} -> var2var' t
   | Tvar i -> Tvar' i
   | Tarr (a,b) -> Tarr (var2var' a, var2var' b)
@@ -252,12 +252,12 @@ type abbrev_map = global_reference -> ml_type option
 (*s Delta-reduction of type constants everywhere in a ML type [t].
    [env] is a function of type [ml_type_env]. *)
 
-let type_expand env t = 
+let type_expand env t =
   let rec expand = function
     | Tmeta {contents = Some t} -> expand t
-    | Tglob (r,l) ->    
-	(match env r with 
-	   | Some mlt -> expand (type_subst_list l mlt) 
+    | Tglob (r,l) ->
+	(match env r with
+	   | Some mlt -> expand (type_subst_list l mlt)
 	   | None -> Tglob (r, List.map expand l))
     | Tarr (a,b) -> Tarr (expand a, expand b)
     | a -> a
@@ -267,13 +267,13 @@ let type_expand env t =
 
 let is_arrow = function Tarr _ -> true | _ -> false
 
-let type_weak_expand env t = 
+let type_weak_expand env t =
   let rec expand = function
     | Tmeta {contents = Some t} -> expand t
-    | Tglob (r,l) as t ->    
-	(match env r with 
-	   | Some mlt -> 
-	       let u = expand (type_subst_list l mlt) in 
+    | Tglob (r,l) as t ->
+	(match env r with
+	   | Some mlt ->
+	       let u = expand (type_subst_list l mlt) in
 	       if is_arrow u then u else t
 	   | None -> t)
     | Tarr (a,b) -> Tarr (a, expand b)
@@ -282,16 +282,16 @@ let type_weak_expand env t =
 
 (*s Generating a signature from a ML type. *)
 
-let type_to_sign env t = match type_expand env t with 
-  | Tdummy d -> Kill d 
+let type_to_sign env t = match type_expand env t with
+  | Tdummy d -> Kill d
   | _ -> Keep
 
-let type_to_signature env t = 
-  let rec f = function 
-    | Tmeta {contents = Some t} -> f t 
+let type_to_signature env t =
+  let rec f = function
+    | Tmeta {contents = Some t} -> f t
     | Tarr (Tdummy d, b) -> Kill d :: f b
     | Tarr (_, b) -> Keep :: f b
-    | _ -> [] 
+    | _ -> []
   in f (type_expand env t)
 
 let isKill = function Kill _ -> true | _ -> false
@@ -302,34 +302,34 @@ let sign_of_id i = if i = dummy_name then Kill Kother else Keep
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
-let type_expunge env t = 
-  let s = type_to_signature env t in 
-  if s = [] then t 
-  else if List.mem Keep s then 
-    let rec f t s = 
-      if List.exists isKill s then 
-	match t with 
+let type_expunge env t =
+  let s = type_to_signature env t in
+  if s = [] then t
+  else if List.mem Keep s then
+    let rec f t s =
+      if List.exists isKill s then
+	match t with
 	  | Tmeta {contents = Some t} -> f t s
-	  | Tarr (a,b) -> 
-	      let t = f b (List.tl s) in 
-	      if List.hd s = Keep then Tarr (a, t) else t  
+	  | Tarr (a,b) ->
+	      let t = f b (List.tl s) in
+	      if List.hd s = Keep then Tarr (a, t) else t
 	  | Tglob (r,l) ->
-	      (match env r with 
+	      (match env r with
 		 | Some mlt -> f (type_subst_list l mlt) s
 		 | None -> assert false)
 	  | _ -> assert false
-      else t 
-    in f t s 
-  else if List.mem (Kill Kother) s then 
-    Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t))) 
+      else t
+    in f t s
+  else if List.mem (Kill Kother) s then
+    Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t)))
   else snd (type_decomp (type_weak_expand env t))
 
 (*S Generic functions over ML ast terms. *)
 
-(*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care 
+(*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
    of the number of bingings crossed before reaching the [MLrel]. *)
 
-let ast_iter_rel f = 
+let ast_iter_rel f =
   let rec iter n = function
     | MLrel i -> f (i-n)
     | MLlam (_,a) -> iter (n+1) a
@@ -341,7 +341,7 @@ let ast_iter_rel f =
     | MLcons (_,_,l) ->  List.iter (iter n) l
     | MLmagic a -> iter n a
     | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
-  in iter 0 
+  in iter 0
 
 (*s Map over asts. *)
 
@@ -361,18 +361,18 @@ let ast_map f = function
 
 let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a)
 
-let ast_map_lift f n = function 
+let ast_map_lift f n = function
   | MLlam (i,a) -> MLlam (i, f (n+1) a)
   | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
   | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v)
-  | MLfix (i,ids,v) -> 
+  | MLfix (i,ids,v) ->
       let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
   | MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
   | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a	
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
 
-(*s Iter over asts. *) 
+(*s Iter over asts. *)
 
 let ast_iter_case f (c,ids,a) = f a
 
@@ -390,23 +390,23 @@ let ast_iter f = function
 
 (*s [ast_occurs k t] returns [true] if [(Rel k)] occurs in [t]. *)
 
-let ast_occurs k t = 
-  try 
-    ast_iter_rel (fun i -> if i = k then raise Found) t; false 
+let ast_occurs k t =
+  try
+    ast_iter_rel (fun i -> if i = k then raise Found) t; false
   with Found -> true
 
-(*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)] 
+(*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)]
    in [t] with [k<=i<=k'] *)
 
-let ast_occurs_itvl k k' t = 
-  try 
-    ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false 
+let ast_occurs_itvl k k' t =
+  try
+    ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
   with Found -> true
 
 (*s Number of occurences of [Rel k] and [Rel 1] in [t]. *)
 
 let nb_occur_k k t =
-  let cpt = ref 0 in 
+  let cpt = ref 0 in
   ast_iter_rel (fun i -> if i = k then incr cpt) t;
   !cpt
 
@@ -415,19 +415,19 @@ let nb_occur t = nb_occur_k 1 t
 (* Number of occurences of [Rel 1] in [t], with special treatment of match:
    occurences in different branches aren't added, but we rather use max. *)
 
-let nb_occur_match = 
-  let rec nb k = function 
+let nb_occur_match =
+  let rec nb k = function
     | MLrel i -> if i = k then 1 else 0
-    | MLcase(_,a,v) -> 
+    | MLcase(_,a,v) ->
         (nb k a) +
-	Array.fold_left 
+	Array.fold_left
 	  (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
-    | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b) 
-    | MLfix (_,ids,v) -> let k = k+(Array.length ids) in 
+    | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b)
+    | MLfix (_,ids,v) -> let k = k+(Array.length ids) in
       Array.fold_left (fun r a -> r+(nb k a)) 0 v
     | MLlam (_,a) -> nb (k+1) a
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
-    | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l 
+    | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
     | MLmagic a -> nb k a
     | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
   in nb 1
@@ -435,7 +435,7 @@ let nb_occur_match =
 (*s Lifting on terms.
     [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *)
 
-let ast_lift k t = 
+let ast_lift k t =
   let rec liftrec n = function
     | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
     | a -> ast_map_lift liftrec n a
@@ -443,45 +443,45 @@ let ast_lift k t =
 
 let ast_pop t = ast_lift (-1) t
 
-(*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ... 
+(*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ...
   Rel (k'+k)] and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *)
 
-let permut_rels k k' = 
+let permut_rels k k' =
   let rec permut n = function
     | MLrel i as a ->
 	let i' = i-n in
-	if i'<1 || i'>k+k' then a 
+	if i'<1 || i'>k+k' then a
 	else if i'<=k then MLrel (i+k')
 	else MLrel (i-k)
     | a -> ast_map_lift permut n a
-  in permut 0  
+  in permut 0
 
-(*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. 
+(*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t].
     Lifting (of one binder) is done at the same time. *)
 
 let ast_subst e =
   let rec subst n = function
     | MLrel i as a ->
-	let i' = i-n in 
+	let i' = i-n in
 	if i'=1 then ast_lift n e
-	else if i'<1 then a 
+	else if i'<1 then a
 	else MLrel (i-1)
     | a -> ast_map_lift subst n a
   in subst 0
 
-(*s Generalized substitution. 
-   [gen_subst v d t] applies to [t] the substitution coded in the 
-   [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies 
+(*s Generalized substitution.
+   [gen_subst v d t] applies to [t] the substitution coded in the
+   [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies
    to [Rel] greater than [Array.length v]. *)
 
-let gen_subst v d t = 
+let gen_subst v d t =
   let rec subst n = function
-    | MLrel i as a -> 
-	let i'= i-n in 
-	if i' < 1 then a 
-	else if i' <= Array.length v then 
-	  ast_lift n v.(i'-1) 
-	else MLrel (i+d) 
+    | MLrel i as a ->
+	let i'= i-n in
+	if i' < 1 then a
+	else if i' <= Array.length v then
+	  ast_lift n v.(i'-1)
+	else MLrel (i+d)
     | a -> ast_map_lift subst n a
   in subst 0 t
 
@@ -490,7 +490,7 @@ let gen_subst v d t =
 (*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
     [[idn;...;id1]] and the term [t]. *)
 
-let collect_lams = 
+let collect_lams =
   let rec collect acc = function
     | MLlam(id,t) -> collect (id::acc) t
     | x           -> acc,x
@@ -498,50 +498,50 @@ let collect_lams =
 
 (*s [collect_n_lams] does the same for a precise number of [MLlam]. *)
 
-let collect_n_lams = 
-  let rec collect acc n t = 
-    if n = 0 then acc,t 
-    else match t with 
+let collect_n_lams =
+  let rec collect acc n t =
+    if n = 0 then acc,t
+    else match t with
       | MLlam(id,t) -> collect (id::acc) (n-1) t
       | _ -> assert false
-  in collect [] 
+  in collect []
 
 (*s [remove_n_lams] just removes some [MLlam]. *)
 
-let rec remove_n_lams n t = 
-  if n = 0 then t  
-  else match t with 
+let rec remove_n_lams n t =
+  if n = 0 then t
+  else match t with
       | MLlam(_,t) -> remove_n_lams (n-1) t
       | _ -> assert false
 
 (*s [nb_lams] gives the number of head [MLlam]. *)
 
-let rec nb_lams = function 
+let rec nb_lams = function
   | MLlam(_,t) -> succ (nb_lams t)
-  | _ -> 0 
+  | _ -> 0
 
 (*s [named_lams] does the converse of [collect_lams]. *)
 
-let rec named_lams ids a = match ids with 
-  | [] -> a 
+let rec named_lams ids a = match ids with
+  | [] -> a
   | id :: ids -> named_lams ids (MLlam (id,a))
 
 (*s The same in anonymous version. *)
 
-let rec anonym_lams a = function 
-  | 0 -> a 
+let rec anonym_lams a = function
+  | 0 -> a
   | n -> anonym_lams (MLlam (anonymous,a)) (pred n)
 
 (*s Idem for [dummy_name]. *)
 
-let rec dummy_lams a = function 
-  | 0 -> a 
+let rec dummy_lams a = function
+  | 0 -> a
   | n -> dummy_lams (MLlam (dummy_name,a)) (pred n)
 
 (*s mixed according to a signature. *)
 
-let rec anonym_or_dummy_lams a = function 
-  | [] -> a 
+let rec anonym_or_dummy_lams a = function
+  | [] -> a
   | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
   | Kill _ :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s)
 
@@ -549,41 +549,41 @@ let rec anonym_or_dummy_lams a = function
 
 (*s The following function creates [MLrel n;...;MLrel 1] *)
 
-let rec eta_args n = 
+let rec eta_args n =
   if n = 0 then [] else (MLrel n)::(eta_args (pred n))
 
 (*s Same, but filtered by a signature. *)
 
-let rec eta_args_sign n = function 
-  | [] -> [] 
-  | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s) 
+let rec eta_args_sign n = function
+  | [] -> []
+  | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s)
   | Kill _ :: s -> eta_args_sign (n-1) s
 
 (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
 
-let rec test_eta_args_lift k n = function 
+let rec test_eta_args_lift k n = function
   | [] -> n=0
   | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
 
 (*s Computes an eta-reduction. *)
 
-let eta_red e = 
-  let ids,t = collect_lams e in 
+let eta_red e =
+  let ids,t = collect_lams e in
   let n = List.length ids in
-  if n = 0 then e 
-  else match t with 
-    | MLapp (f,a) -> 
-	let m = List.length a in 
-	let ids,body,args = 
-	  if m = n then 
+  if n = 0 then e
+  else match t with
+    | MLapp (f,a) ->
+	let m = List.length a in
+	let ids,body,args =
+	  if m = n then
 	    [], f, a
-	  else if m < n then 
-	    snd (list_chop (n-m) ids), f, a 
+	  else if m < n then
+	    snd (list_chop (n-m) ids), f, a
 	  else (* m > n *)
-	    let a1,a2 = list_chop (m-n) a in 
+	    let a1,a2 = list_chop (m-n) a in
 	    [], MLapp (f,a1), a2
-	in 
-	let p = List.length args in  
+	in
+	let p = List.length args in
 	if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body)
 	then named_lams ids (ast_lift (-p) body)
 	else e
@@ -592,24 +592,24 @@ let eta_red e =
 (*s Computes all head linear beta-reductions possible in [(t a)].
   Non-linear head beta-redex become let-in. *)
 
-let rec linear_beta_red a t = match a,t with  
-  | [], _ -> t 
+let rec linear_beta_red a t = match a,t with
+  | [], _ -> t
   | a0::a, MLlam (id,t) ->
       (match nb_occur_match t with
 	 | 0 -> linear_beta_red a (ast_pop t)
 	 | 1 -> linear_beta_red a (ast_subst a0 t)
-	 | _ -> 
-	     let a = List.map (ast_lift 1) a in 
+	 | _ ->
+	     let a = List.map (ast_lift 1) a in
 	     MLletin (id, a0, linear_beta_red a t))
   | _ -> MLapp (t, a)
 
-(*s Applies a substitution [s] of constants by their body, plus 
-  linear beta reductions at modified positions. *)  
+(*s Applies a substitution [s] of constants by their body, plus
+  linear beta reductions at modified positions. *)
 
-let rec ast_glob_subst s t = match t with 
-  | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> 
-      let a = List.map (ast_glob_subst s) a in 
-      (try linear_beta_red a (Refmap.find refe s) 
+let rec ast_glob_subst s t = match t with
+  | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
+      let a = List.map (ast_glob_subst s) a in
+      (try linear_beta_red a (Refmap.find refe s)
        with Not_found -> MLapp (f, a))
   | MLglob ((ConstRef kn) as refe) ->
       (try Refmap.find refe s with Not_found -> t)
@@ -619,114 +619,114 @@ let rec ast_glob_subst s t = match t with
 (*S Auxiliary functions used in simplification of ML cases. *)
 
 (*s [check_and_generalize (r0,l,c)] transforms any [MLcons(r0,l)] in [MLrel 1]
-  and raises [Impossible] if any variable in [l] occurs outside such a 
+  and raises [Impossible] if any variable in [l] occurs outside such a
   [MLcons] *)
 
-let check_and_generalize (r0,l,c) = 
-  let nargs = List.length l in 
-  let rec genrec n = function 
-    | MLrel i as c -> 
-	let i' = i-n in 
-	if i'<1 then c 
-	else if i'>nargs then MLrel (i-nargs+1) 
+let check_and_generalize (r0,l,c) =
+  let nargs = List.length l in
+  let rec genrec n = function
+    | MLrel i as c ->
+	let i' = i-n in
+	if i'<1 then c
+	else if i'>nargs then MLrel (i-nargs+1)
 	else raise Impossible
-    | MLcons(_,r,args) when r=r0 && (test_eta_args_lift n nargs args) -> 
-	MLrel (n+1) 
+    | MLcons(_,r,args) when r=r0 && (test_eta_args_lift n nargs args) ->
+	MLrel (n+1)
     | a -> ast_map_lift genrec n a
-  in genrec 0 c  
+  in genrec 0 c
 
-(*s [check_generalizable_case] checks if all branches can be seen as the 
-  same function [f] applied to the term matched. It is a generalized version 
+(*s [check_generalizable_case] checks if all branches can be seen as the
+  same function [f] applied to the term matched. It is a generalized version
   of the identity case optimization. *)
 
-(* CAVEAT: this optimization breaks typing in some special case. example: 
+(* CAVEAT: this optimization breaks typing in some special case. example:
    [type 'x a = A]. Then [let f = function A -> A] has type ['x a -> 'y a],
    which is incompatible with the type of [let f x = x].
-   By default, we brutally disable this optim except for some known types: 
+   By default, we brutally disable this optim except for some known types:
    [bool], [sumbool], [sumor] *)
 
-let generalizable_list = 
+let generalizable_list =
   let datatypes = MPfile (dirpath_of_string "Coq.Init.Datatypes")
   and specif = MPfile (dirpath_of_string "Coq.Init.Specif")
-  in 
-  [ make_kn datatypes empty_dirpath (mk_label "bool"); 
+  in
+  [ make_kn datatypes empty_dirpath (mk_label "bool");
     make_kn specif empty_dirpath (mk_label "sumbool");
     make_kn specif empty_dirpath (mk_label "sumor") ]
 
-let check_generalizable_case unsafe br = 
-  if not unsafe then 
-    (match br.(0) with 
+let check_generalizable_case unsafe br =
+  if not unsafe then
+    (match br.(0) with
      | ConstructRef ((kn,_),_), _, _ ->
 	 if not (List.mem kn generalizable_list) then raise Impossible
-     | _ -> assert false); 
-  let f = check_and_generalize br.(0) in 
-  for i = 1 to Array.length br - 1 do 
-    if check_and_generalize br.(i) <> f then raise Impossible 
+     | _ -> assert false);
+  let f = check_and_generalize br.(0) in
+  for i = 1 to Array.length br - 1 do
+    if check_and_generalize br.(i) <> f then raise Impossible
   done; f
 
 (*s Detecting similar branches of a match *)
 
-(* If several branches of a match are equal (and independent from their 
-   patterns) we will print them using a _ pattern. If _all_ branches 
+(* If several branches of a match are equal (and independent from their
+   patterns) we will print them using a _ pattern. If _all_ branches
    are equal, we remove the match.
 *)
 
-let common_branches br = 
-  let tab = Hashtbl.create 13 in 
-  for i = 0 to Array.length br - 1 do 
-    let (r,ids,t) = br.(i) in 
-    let n = List.length ids in 
-    if not (ast_occurs_itvl 1 n t) then 
-       let t = ast_lift (-n) t in 
-       let l = try Hashtbl.find tab t with Not_found -> [] in 
+let common_branches br =
+  let tab = Hashtbl.create 13 in
+  for i = 0 to Array.length br - 1 do
+    let (r,ids,t) = br.(i) in
+    let n = List.length ids in
+    if not (ast_occurs_itvl 1 n t) then
+       let t = ast_lift (-n) t in
+       let l = try Hashtbl.find tab t with Not_found -> [] in
        Hashtbl.replace tab t (i::l)
-  done; 
-  let best = ref [] in 
-  Hashtbl.iter 
-    (fun _ l -> if List.length l > List.length !best then best := l) tab; 
+  done;
+  let best = ref [] in
+  Hashtbl.iter
+    (fun _ l -> if List.length l > List.length !best then best := l) tab;
   if List.length !best < 2 then [] else !best
 
 (*s If all branches are functions, try to permut the case and the functions. *)
 
-let rec merge_ids ids ids' = match ids,ids' with 
-  | [],l -> l 
+let rec merge_ids ids ids' = match ids,ids' with
+  | [],l -> l
   | l,[] -> l
-  | i::ids, i'::ids' -> 
+  | i::ids, i'::ids' ->
       (if i = dummy_name then i' else i) :: (merge_ids ids ids')
 
 let is_exn = function MLexn _ -> true | _ -> false
 
-let rec permut_case_fun br acc = 
-  let nb = ref max_int in 
-  Array.iter (fun (_,_,t) -> 
-		let ids, c = collect_lams t in 
-		let n = List.length ids in 
-		if (n < !nb) && (not (is_exn c)) then nb := n) br; 
-  if !nb = max_int || !nb = 0 then ([],br) 
+let rec permut_case_fun br acc =
+  let nb = ref max_int in
+  Array.iter (fun (_,_,t) ->
+		let ids, c = collect_lams t in
+		let n = List.length ids in
+		if (n < !nb) && (not (is_exn c)) then nb := n) br;
+  if !nb = max_int || !nb = 0 then ([],br)
   else begin
-    let br = Array.copy br in 
-    let ids = ref [] in  
-    for i = 0 to Array.length br - 1 do 
-      let (r,l,t) = br.(i) in 
-      let local_nb = nb_lams t in 
+    let br = Array.copy br in
+    let ids = ref [] in
+    for i = 0 to Array.length br - 1 do
+      let (r,l,t) = br.(i) in
+      let local_nb = nb_lams t in
       if local_nb < !nb then (* t = MLexn ... *)
 	br.(i) <- (r,l,remove_n_lams local_nb t)
       else begin
-	let local_ids,t = collect_n_lams !nb t in 
-	ids := merge_ids !ids local_ids; 
+	let local_ids,t = collect_n_lams !nb t in
+	ids := merge_ids !ids local_ids;
 	br.(i) <- (r,l,permut_rels !nb (List.length l) t)
       end
-    done; 
+    done;
     (!ids,br)
   end
-  
+
 (*S Generalized iota-reduction. *)
 
-(* Definition of a generalized iota-redex: it's a [MLcase(e,_)] 
-   with [(is_iota_gen e)=true]. Any generalized iota-redex is 
+(* Definition of a generalized iota-redex: it's a [MLcase(e,_)]
+   with [(is_iota_gen e)=true]. Any generalized iota-redex is
    transformed into beta-redexes. *)
 
-let rec is_iota_gen = function 
+let rec is_iota_gen = function
   | MLcons _ -> true
   | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
   | _ -> false
@@ -735,21 +735,21 @@ let constructor_index = function
   | ConstructRef (_,j) -> pred j
   | _ -> assert false
 
-let iota_gen br = 
-  let rec iota k = function 
+let iota_gen br =
+  let rec iota k = function
     | MLcons (i,r,a) ->
 	let (_,ids,c) = br.(constructor_index r) in
 	let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
-	let c = ast_lift k c in 
+	let c = ast_lift k c in
 	MLapp (c,a)
-    | MLcase(i,e,br') -> 
-	let new_br = 
+    | MLcase(i,e,br') ->
+	let new_br =
 	  Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br'
 	in MLcase(i,e, new_br)
     | _ -> assert false
-  in iota 0 
+  in iota 0
 
-let is_atomic = function 
+let is_atomic = function
   | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
   | _ -> false
 
@@ -760,131 +760,131 @@ let is_atomic = function
 let rec simpl o = function
   | MLapp (f, []) ->
       simpl o f
-  | MLapp (f, a) -> 
+  | MLapp (f, a) ->
       simpl_app o (List.map (simpl o) a) (simpl o f)
   | MLcase (i,e,br) ->
-      let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in 
-      simpl_case o i br (simpl o e) 
-  | MLletin(id,c,e) -> 
-      let e = (simpl o e) in 
-      if 
+      let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
+      simpl_case o i br (simpl o e)
+  | MLletin(id,c,e) ->
+      let e = (simpl o e) in
+      if
 	(id = dummy_name) || (is_atomic c) || (is_atomic e) ||
 	(let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let))
-      then 
+      then
 	simpl o (ast_subst c e)
-      else 
+      else
 	MLletin(id, simpl o c, e)
-  | MLfix(i,ids,c) -> 
-      let n = Array.length ids in 
-      if ast_occurs_itvl 1 n c.(i) then 
+  | MLfix(i,ids,c) ->
+      let n = Array.length ids in
+      if ast_occurs_itvl 1 n c.(i) then
 	MLfix (i, ids, Array.map (simpl o) c)
       else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
-  | a -> ast_map (simpl o) a 
+  | a -> ast_map (simpl o) a
 
-and simpl_app o a = function  
+and simpl_app o a = function
   | MLapp (f',a') -> simpl_app o (a'@a) f'
-  | MLlam (id,t) when id = dummy_name -> 
+  | MLlam (id,t) when id = dummy_name ->
       simpl o (MLapp (ast_pop t, List.tl a))
   | MLlam (id,t) -> (* Beta redex *)
       (match nb_occur_match t with
 	 | 0 -> simpl o (MLapp (ast_pop t, List.tl a))
-	 | 1 when o.opt_lin_beta -> 
+	 | 1 when o.opt_lin_beta ->
 	     simpl o (MLapp (ast_subst (List.hd a) t, List.tl a))
-	 | _ -> 
+	 | _ ->
 	     let a' = List.map (ast_lift 1) (List.tl a) in
 	     simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
-  | MLletin (id,e1,e2) when o.opt_let_app -> 
+  | MLletin (id,e1,e2) when o.opt_let_app ->
       (* Application of a letin: we push arguments inside *)
       MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
-  | MLcase (i,e,br) when o.opt_case_app -> 
+  | MLcase (i,e,br) when o.opt_case_app ->
       (* Application of a case: we push arguments inside *)
-      let br' = 
-	Array.map 
-      	  (fun (n,l,t) -> 
+      let br' =
+	Array.map
+      	  (fun (n,l,t) ->
 	     let k = List.length l in
 	     let a' = List.map (ast_lift k) a in
-      	     (n, l, simpl o (MLapp (t,a')))) br 
-      in simpl o (MLcase (i,e,br')) 
-  | (MLdummy | MLexn _) as e -> e 
+      	     (n, l, simpl o (MLapp (t,a')))) br
+      in simpl o (MLcase (i,e,br'))
+  | (MLdummy | MLexn _) as e -> e
 	(* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
-and simpl_case o i br e = 
+and simpl_case o i br e =
   if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
     simpl o (iota_gen br e)
-  else 
+  else
     try (* Does a term [f] exist such that each branch is [(f e)] ? *)
       if not o.opt_case_idr then raise Impossible;
-      let f = check_generalizable_case o.opt_case_idg br in 
+      let f = check_generalizable_case o.opt_case_idg br in
       simpl o (MLapp (MLlam (anonymous,f),[e]))
-    with Impossible -> 
+    with Impossible ->
       (* Detect common branches *)
       let common_br = if not o.opt_case_cst then [] else common_branches br in
-      if List.length common_br = Array.length br && br <> [||] then 
+      if List.length common_br = Array.length br && br <> [||] then
 	let (_,ids,t) = br.(0) in ast_lift (-List.length ids) t
-      else 
-	let new_i = (fst i, common_br) in 
+      else
+	let new_i = (fst i, common_br) in
 	(* Swap the case and the lam if possible *)
-	if o.opt_case_fun 
-	then 
-	  let ids,br = permut_case_fun br [] in 
-	  let n = List.length ids in 
+	if o.opt_case_fun
+	then
+	  let ids,br = permut_case_fun br [] in
+	  let n = List.length ids in
 	  if n <> 0 then named_lams ids (MLcase (new_i,ast_lift n e, br))
-	  else MLcase (new_i,e,br) 
+	  else MLcase (new_i,e,br)
 	else MLcase (new_i,e,br)
 
-let rec post_simpl = function 
-  | MLletin(_,c,e) when (is_atomic (eta_red c)) -> 
+let rec post_simpl = function
+  | MLletin(_,c,e) when (is_atomic (eta_red c)) ->
       post_simpl (ast_subst (eta_red c) e)
-  | a -> ast_map post_simpl a 
+  | a -> ast_map post_simpl a
 
-(*S Local prop elimination. *) 
+(*S Local prop elimination. *)
 (* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
 
-(*s In a list, it selects only the elements corresponding to a [Keep] 
+(*s In a list, it selects only the elements corresponding to a [Keep]
    in the boolean list [l]. *)
 
-let rec select_via_bl l args = match l,args with 
+let rec select_via_bl l args = match l,args with
   | [],_ -> args
   | Keep::l,a::args -> a :: (select_via_bl l args)
   | Kill _::l,a::args -> select_via_bl l args
-  | _ -> assert false 
+  | _ -> assert false
 
 (*s [kill_some_lams] removes some head lambdas according to the signature [bl].
    This list is build on the identifier list model: outermost lambda
-   is on the right. 
-   [Rels] corresponding to removed lambdas are supposed not to occur, and 
+   is on the right.
+   [Rels] corresponding to removed lambdas are supposed not to occur, and
    the other [Rels] are made correct via a [gen_subst].
    Output is not directly a [ml_ast], compose with [named_lams] if needed. *)
 
 let kill_some_lams bl (ids,c) =
   let n = List.length bl in
-  let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in 
+  let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in
   if n = n' then ids,c
-  else if n' = 0 then [],ast_lift (-n) c 
+  else if n' = 0 then [],ast_lift (-n) c
   else begin
-    let v = Array.make n MLdummy in 
-    let rec parse_ids i j = function 
+    let v = Array.make n MLdummy in
+    let rec parse_ids i j = function
       | [] -> ()
       | Keep :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l
       | Kill _ :: l -> parse_ids (i+1) j l
-    in parse_ids 0 1 bl ; 
+    in parse_ids 0 1 bl ;
     select_via_bl bl ids, gen_subst v (n'-n) c
   end
 
-(*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding 
-  to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or 
+(*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding
+  to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or
   if there is no lambda left at all. *)
 
-let kill_dummy_lams c = 
-  let ids,c = collect_lams c in 
+let kill_dummy_lams c =
+  let ids,c = collect_lams c in
   let bl = List.map sign_of_id ids in
-  if (List.mem Keep bl) && (List.exists isKill bl) then 
-    let ids',c = kill_some_lams bl (ids,c) in 
+  if (List.mem Keep bl) && (List.exists isKill bl) then
+    let ids',c = kill_some_lams bl (ids,c) in
     ids, named_lams ids' c
   else raise Impossible
 
-(*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c] 
+(*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c]
    and a signature [s] and builds a eta-long version. *)
 
 (* For example, if [s = [Keep;Keep;Kill Prop;Keep]] then the output is :
@@ -892,137 +892,137 @@ let kill_dummy_lams c =
 
 let eta_expansion_sign s (ids,c) =
   let rec abs ids rels i = function
-    | [] -> 
+    | [] ->
 	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
-	in ids, MLapp (ast_lift (i-1) c, a) 
-    | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l 
+	in ids, MLapp (ast_lift (i-1) c, a)
+    | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l
     | Kill _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l
   in abs ids [] 1 s
 
-(*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] 
-  in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas 
+(*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e]
+  in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas
   corresponding to [Del] in [s]. *)
 
-let case_expunge s e = 
-  let m = List.length s in 
-  let n = nb_lams e in 
-  let p = if m <= n then collect_n_lams m e 
-  else eta_expansion_sign (list_skipn n s) (collect_lams e) in 
+let case_expunge s e =
+  let m = List.length s in
+  let n = nb_lams e in
+  let p = if m <= n then collect_n_lams m e
+  else eta_expansion_sign (list_skipn n s) (collect_lams e) in
   kill_some_lams (List.rev s) p
 
-(*s [term_expunge] takes a function [fun idn ... id1 -> c] 
-  and a signature [s] and remove dummy lams. The difference 
-  with [case_expunge] is that we here leave one dummy lambda 
+(*s [term_expunge] takes a function [fun idn ... id1 -> c]
+  and a signature [s] and remove dummy lams. The difference
+  with [case_expunge] is that we here leave one dummy lambda
   if all lambdas are logical dummy. *)
 
 let term_expunge s (ids,c) =
-  if s = [] then c 
-  else 
-    let ids,c = kill_some_lams (List.rev s) (ids,c) in 
-    if ids = [] && List.mem (Kill Kother) s then 
+  if s = [] then c
+  else
+    let ids,c = kill_some_lams (List.rev s) (ids,c) in
+    if ids = [] && List.mem (Kill Kother) s then
       MLlam (dummy_name, ast_lift 1 c)
     else named_lams ids c
 
-(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and 
-  purge the args of [t0] corresponding to a [dummy_name]. 
-  It makes eta-expansion if needed. *) 
+(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and
+  purge the args of [t0] corresponding to a [dummy_name].
+  It makes eta-expansion if needed. *)
 
 let kill_dummy_args ids t0 t =
-  let m = List.length ids in 
+  let m = List.length ids in
   let bl = List.rev_map sign_of_id ids in
-  let rec killrec n = function 
-    | MLapp(e, a) when e = ast_lift n t0 -> 
-	let k = max 0 (m - (List.length a)) in 
-	let a = List.map (killrec n) a in  
-	let a = List.map (ast_lift k) a in 
-	let a = select_via_bl bl (a @ (eta_args k)) in 
-	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a)) 
-    | e when e = ast_lift n t0 -> 
-	let a = select_via_bl bl (eta_args m) in 
+  let rec killrec n = function
+    | MLapp(e, a) when e = ast_lift n t0 ->
+	let k = max 0 (m - (List.length a)) in
+	let a = List.map (killrec n) a in
+	let a = List.map (ast_lift k) a in
+	let a = select_via_bl bl (a @ (eta_args k)) in
+	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
+    | e when e = ast_lift n t0 ->
+	let a = select_via_bl bl (eta_args m) in
 	named_lams ids (MLapp (ast_lift m e, a))
-    | e -> ast_map_lift killrec n e 
-  in killrec 0 t 
+    | e -> ast_map_lift killrec n e
+  in killrec 0 t
 
 (*s The main function for local [dummy] elimination. *)
 
-let rec kill_dummy = function 
-  | MLfix(i,fi,c) -> 
-      (try 
-	 let ids,c = kill_dummy_fix i fi c in 
+let rec kill_dummy = function
+  | MLfix(i,fi,c) ->
+      (try
+	 let ids,c = kill_dummy_fix i fi c in
 	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1))
        with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
-  | MLapp (MLfix (i,fi,c),a) -> 
-      (try 
-	 let ids,c = kill_dummy_fix i fi c in 
-	 let a = List.map (fun t -> ast_lift 1 (kill_dummy t)) a in 
+  | MLapp (MLfix (i,fi,c),a) ->
+      (try
+	 let ids,c = kill_dummy_fix i fi c in
+	 let a = List.map (fun t -> ast_lift 1 (kill_dummy t)) a in
 	 let e = kill_dummy_args ids (MLrel 1) (MLapp (MLrel 1,a)) in
-	 ast_subst (MLfix (i,fi,c)) e  
-       with Impossible -> 
+	 ast_subst (MLfix (i,fi,c)) e
+       with Impossible ->
 	 MLapp(MLfix(i,fi,Array.map kill_dummy c),List.map kill_dummy a))
-  | MLletin(id, MLfix (i,fi,c),e) -> 
-      (try 
+  | MLletin(id, MLfix (i,fi,c),e) ->
+      (try
 	 let ids,c = kill_dummy_fix i fi c in
-	 let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in 
+	 let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in
 	 MLletin(id, MLfix(i,fi,c),e)
-      with Impossible -> 
+      with Impossible ->
 	MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
-  | MLletin(id,c,e) -> 
-      (try 
-	 let ids,c = kill_dummy_lams c in 
-	 let e = kill_dummy_args ids (MLrel 1) e in 
-	 MLletin (id, kill_dummy c,kill_dummy e) 
+  | MLletin(id,c,e) ->
+      (try
+	 let ids,c = kill_dummy_lams c in
+	 let e = kill_dummy_args ids (MLrel 1) e in
+	 MLletin (id, kill_dummy c,kill_dummy e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
   | a -> ast_map kill_dummy a
 
-and kill_dummy_fix i fi c = 
-  let n = Array.length fi in 
-  let ids,ci = kill_dummy_lams c.(i) in 
-  let c = Array.copy c in c.(i) <- ci; 
-  for j = 0 to (n-1) do 
-    c.(j) <- kill_dummy (kill_dummy_args ids (MLrel (n-i)) c.(j)) 
+and kill_dummy_fix i fi c =
+  let n = Array.length fi in
+  let ids,ci = kill_dummy_lams c.(i) in
+  let c = Array.copy c in c.(i) <- ci;
+  for j = 0 to (n-1) do
+    c.(j) <- kill_dummy (kill_dummy_args ids (MLrel (n-i)) c.(j))
   done;
   ids,c
 
 (*s Putting things together. *)
 
-let normalize a = 
-  let o = optims () in 
-  let a = simpl o a in 
+let normalize a =
+  let o = optims () in
+  let a = simpl o a in
   if o.opt_kill_dum then post_simpl (kill_dummy a) else a
 
 (*S Special treatment of fixpoint for pretty-printing purpose. *)
 
-let general_optimize_fix f ids n args m c = 
-  let v = Array.make n 0 in 
+let general_optimize_fix f ids n args m c =
+  let v = Array.make n 0 in
   for i=0 to (n-1) do v.(i)<-i done;
-  let aux i = function 
-    | MLrel j when v.(j-1)>=0 -> 
+  let aux i = function
+    | MLrel j when v.(j-1)>=0 ->
 	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
     | _ -> raise Impossible
-  in list_iter_i aux args; 
+  in list_iter_i aux args;
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
-  let new_f = anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in  
+  let new_f = anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in
   let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
   MLfix(0,[|f|],[|new_c|])
 
-let optimize_fix a = 
-  if not (optims()).opt_fix_fun then a 
+let optimize_fix a =
+  if not (optims()).opt_fix_fun then a
   else
-    let ids,a' = collect_lams a in 
-    let n = List.length ids in 
-    if n = 0 then a 
-    else match a' with 
+    let ids,a' = collect_lams a in
+    let n = List.length ids in
+    if n = 0 then a
+    else match a' with
       | MLfix(_,[|f|],[|c|]) ->
-	  let new_f = MLapp (MLrel (n+1),eta_args n) in 
+	  let new_f = MLapp (MLrel (n+1),eta_args n) in
 	  let new_c = named_lams ids (normalize (ast_subst new_f c))
 	  in MLfix(0,[|f|],[|new_c|])
       | MLapp(a',args) ->
-	  let m = List.length args in 
-	  (match a' with 
-	     | MLfix(_,_,_) when 
-		 (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a') 
+	  let m = List.length args in
+	  (match a' with
+	     | MLfix(_,_,_) when
+		 (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a')
 		 -> a'
-	     | MLfix(_,[|f|],[|c|]) -> 
+	     | MLfix(_,[|f|],[|c|]) ->
 		 (try general_optimize_fix f ids n args m c
 		  with Impossible -> a)
 	     | _ -> a)
@@ -1036,7 +1036,7 @@ let rec ml_size = function
   | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
   | MLlam(_,t) -> 1 + ml_size t
   | MLcons(_,_,l) -> ml_size_list l
-  | MLcase(_,t,pv) -> 
+  | MLcase(_,t,pv) ->
       1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
@@ -1057,111 +1057,111 @@ let rec is_constr = function
 (*s Strictness *)
 
 (* A variable is strict if the evaluation of the whole term implies
-   the evaluation of this variable. Non-strict variables can be found 
-   behind Match, for example. Expanding a term [t] is a good idea when 
-   it begins by at least one non-strict lambda, since the corresponding 
+   the evaluation of this variable. Non-strict variables can be found
+   behind Match, for example. Expanding a term [t] is a good idea when
+   it begins by at least one non-strict lambda, since the corresponding
    argument to [t] might be unevaluated in the expanded code. *)
 
 exception Toplevel
 
 let lift n l = List.map ((+) n) l
 
-let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l 
+let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l
 
 (* This function returns a list of de Bruijn indices of non-strict variables,
-   or raises [Toplevel] if it has an internal non-strict variable. 
-   In fact, not all variables are checked for strictness, only the ones which 
-   de Bruijn index is in the candidates list [cand]. The flag [add] controls 
-   the behaviour when going through a lambda: should we add the corresponding 
-   variable to the candidates?  We use this flag to check only the external 
+   or raises [Toplevel] if it has an internal non-strict variable.
+   In fact, not all variables are checked for strictness, only the ones which
+   de Bruijn index is in the candidates list [cand]. The flag [add] controls
+   the behaviour when going through a lambda: should we add the corresponding
+   variable to the candidates?  We use this flag to check only the external
    lambdas, those that will correspond to arguments. *)
 
-let rec non_stricts add cand = function 
-  | MLlam (id,t) -> 
+let rec non_stricts add cand = function
+  | MLlam (id,t) ->
       let cand = lift 1 cand in
       let cand = if add then 1::cand else cand in
       pop 1 (non_stricts add cand t)
-  | MLrel n -> 
-      List.filter ((<>) n) cand  
-  | MLapp (MLrel n, _) -> 
+  | MLrel n ->
+      List.filter ((<>) n) cand
+  | MLapp (MLrel n, _) ->
       List.filter ((<>) n) cand
 	(* In [(x y)] we say that only x is strict. Cf [sig_rec]. We may *)
 	(* gain something if x is replaced by a function like a projection *)
-  | MLapp (t,l)-> 
-      let cand = non_stricts false cand t in 
-      List.fold_left (non_stricts false) cand l 
-  | MLcons (_,_,l) -> 
+  | MLapp (t,l)->
+      let cand = non_stricts false cand t in
+      List.fold_left (non_stricts false) cand l
+  | MLcons (_,_,l) ->
       List.fold_left (non_stricts false) cand l
-  | MLletin (_,t1,t2) -> 
-      let cand = non_stricts false cand t1 in 
+  | MLletin (_,t1,t2) ->
+      let cand = non_stricts false cand t1 in
       pop 1 (non_stricts add (lift 1 cand) t2)
-  | MLfix (_,i,f)-> 
+  | MLfix (_,i,f)->
       let n = Array.length i in
-      let cand = lift n cand in 
-      let cand = Array.fold_left (non_stricts false) cand f in 
+      let cand = lift n cand in
+      let cand = Array.fold_left (non_stricts false) cand f in
       pop n cand
-  | MLcase (_,t,v) -> 
+  | MLcase (_,t,v) ->
       (* The only interesting case: for a variable to be non-strict, *)
       (* it is sufficient that it appears non-strict in at least one branch, *)
       (* so we make an union (in fact a merge). *)
-      let cand = non_stricts false cand t in 
-      Array.fold_left 
-	(fun c (_,i,t)-> 
-	   let n = List.length i in 
-	   let cand = lift n cand in 
+      let cand = non_stricts false cand t in
+      Array.fold_left
+	(fun c (_,i,t)->
+	   let n = List.length i in
+	   let cand = lift n cand in
 	   let cand = pop n (non_stricts add cand t) in
 	   Sort.merge (<=) cand c) [] v
 	(* [merge] may duplicates some indices, but I don't mind. *)
-  | MLmagic t -> 
+  | MLmagic t ->
       non_stricts add cand t
-  | _ -> 
+  | _ ->
       cand
 
 (* The real test: we are looking for internal non-strict variables, so we start
-   with no candidates, and the only positive answer is via the [Toplevel] 
+   with no candidates, and the only positive answer is via the [Toplevel]
    exception. *)
 
-let is_not_strict t = 
+let is_not_strict t =
   try let _ = non_stricts true [] t in false
   with Toplevel -> true
 
 (*s Inlining decision *)
 
-(* [inline_test] answers the following question: 
-   If we could inline [t] (the user said nothing special), 
-   should we inline ? 
-   
-   We expand small terms with at least one non-strict 
+(* [inline_test] answers the following question:
+   If we could inline [t] (the user said nothing special),
+   should we inline ?
+
+   We expand small terms with at least one non-strict
    variable (i.e. a variable that may not be evaluated).
-   
+
    Futhermore we don't expand fixpoints. *)
 
-let inline_test t = 
-  let t1 = eta_red t in 
+let inline_test t =
+  let t1 = eta_red t in
   let t2 = snd (collect_lams t1) in
   not (is_fix t2) && ml_size t < 12 && is_not_strict t
 
-let manual_inline_list = 
-  let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in 
+let manual_inline_list =
+  let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in
   List.map (fun s -> (make_con mp empty_dirpath (mk_label s)))
-    [ "well_founded_induction_type"; "well_founded_induction"; 
+    [ "well_founded_induction_type"; "well_founded_induction";
       "Acc_rect"; "Acc_rec" ; "Acc_iter" ; "Fix" ]
 
-let manual_inline = function 
+let manual_inline = function
   | ConstRef c -> List.mem c manual_inline_list
-  | _ -> false 
+  | _ -> false
 
 (* If the user doesn't say he wants to keep [t], we inline in two cases:
    \begin{itemize}
-   \item the user explicitly requests it 
-   \item [expansion_test] answers that the inlining is a good idea, and 
+   \item the user explicitly requests it
+   \item [expansion_test] answers that the inlining is a good idea, and
    we are free to act (AutoInline is set)
    \end{itemize} *)
 
-let inline r t = 
+let inline r t =
   not (to_keep r) (* The user DOES want to keep it *)
-  && not (is_inline_custom r) 
-  && (to_inline r (* The user DOES want to inline it *) 
+  && not (is_inline_custom r)
+  && (to_inline r (* The user DOES want to inline it *)
      || (auto_inline () && lang () <> Haskell && not (is_projection r)
          && (is_recursor r || manual_inline r || inline_test t)))
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index b5b47490e..4b6b47ab9 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -31,11 +31,11 @@ val put_magic : ml_type * ml_type -> ml_ast -> ml_ast
 
 (*s ML type environment. *)
 
-module Mlenv : sig 
-  type t 
+module Mlenv : sig
+  type t
   val empty : t
-    
-  (* get the n-th more recently entered schema and instantiate it. *) 
+
+  (* get the n-th more recently entered schema and instantiate it. *)
   val get : t -> int -> ml_type
 
   (* Adding a type in an environment, after generalizing free meta *)
@@ -43,7 +43,7 @@ module Mlenv : sig
 
   (* Adding a type with no [Tvar] *)
   val push_type : t -> ml_type -> t
-     
+
   (* Adding a type with no [Tvar] nor [Tmeta] *)
   val push_std_type : t -> ml_type -> t
 end
@@ -57,11 +57,11 @@ val type_maxvar : ml_type -> int
 val type_decomp : ml_type -> ml_type list * ml_type
 val type_recomp : ml_type list * ml_type -> ml_type
 
-val var2var' : ml_type -> ml_type 
+val var2var' : ml_type -> ml_type
 
 type abbrev_map = global_reference -> ml_type option
 
-val type_expand : abbrev_map -> ml_type -> ml_type 
+val type_expand : abbrev_map -> ml_type -> ml_type
 val type_to_sign : abbrev_map -> ml_type -> sign
 val type_to_signature : abbrev_map -> ml_type -> signature
 val type_expunge : abbrev_map -> ml_type -> ml_type
@@ -90,7 +90,7 @@ val nb_lams : ml_ast -> int
 val dummy_lams : ml_ast -> int -> ml_ast
 val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast
 
-val eta_args_sign : int -> signature -> ml_ast list 
+val eta_args_sign : int -> signature -> ml_ast list
 
 (*s Utility functions over ML terms. *)
 
@@ -105,7 +105,7 @@ val ast_subst : ml_ast -> ml_ast -> ml_ast
 
 val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
 
-val normalize : ml_ast -> ml_ast 
+val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
 val inline : global_reference -> ml_ast -> bool
 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 8173ba9c8..0394ea4b7 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -29,12 +29,12 @@ let rec msid_of_mt = function
   | MTwith(mt,_)-> msid_of_mt mt
   | _ -> anomaly "Extraction:the With operator isn't applied to a name"
 
-(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a 
-   [ml_structure]. *) 
+(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
+   [ml_structure]. *)
 
-let struct_iter do_decl do_spec s = 
-  let rec mt_iter = function 
-    | MTident _ -> () 
+let struct_iter do_decl do_spec s =
+  let rec mt_iter = function
+    | MTident _ -> ()
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
     | MTwith (mt,ML_With_type(idl,l,t))->
 	let mp_mt = msid_of_mt mt in
@@ -46,79 +46,79 @@ let struct_iter do_decl do_spec s =
 	mt_iter mt; do_decl (Dtype(r,l,t))
     | MTwith (mt,_)->mt_iter mt
     | MTsig (_, sign) -> List.iter spec_iter sign
-  and spec_iter = function 
+  and spec_iter = function
     | (_,Spec s) -> do_spec s
     | (_,Smodule mt) -> mt_iter mt
     | (_,Smodtype mt) -> mt_iter mt
   in
-  let rec se_iter = function 
+  let rec se_iter = function
     | (_,SEdecl d) -> do_decl d
-    | (_,SEmodule m) -> 
+    | (_,SEmodule m) ->
 	me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
     | (_,SEmodtype m) -> mt_iter m
-  and me_iter = function 
-    | MEident _ -> () 
+  and me_iter = function
+    | MEident _ -> ()
     | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt
     | MEapply (me,me') -> me_iter me; me_iter me'
     | MEstruct (msid, sel) -> List.iter se_iter sel
-  in 
+  in
   List.iter (function (_,sel) -> List.iter se_iter sel) s
 
-(*s Apply some fonctions upon all references in [ml_type], [ml_ast], 
+(*s Apply some fonctions upon all references in [ml_type], [ml_ast],
   [ml_decl], [ml_spec] and [ml_structure]. *)
 
 type do_ref = global_reference -> unit
 
-let record_iter_references do_term = function 
-  | Record l -> List.iter do_term l 
+let record_iter_references do_term = function
+  | Record l -> List.iter do_term l
   | _ -> ()
 
-let type_iter_references do_type t = 
-  let rec iter = function 
-    | Tglob (r,l) -> do_type r; List.iter iter l 
-    | Tarr (a,b) -> iter a; iter b 
-    | _ -> () 
+let type_iter_references do_type t =
+  let rec iter = function
+    | Tglob (r,l) -> do_type r; List.iter iter l
+    | Tarr (a,b) -> iter a; iter b
+    | _ -> ()
   in iter t
 
-let ast_iter_references do_term do_cons do_type a = 
-  let rec iter a = 
+let ast_iter_references do_term do_cons do_type a =
+  let rec iter a =
     ast_iter iter a;
-    match a with 
+    match a with
       | MLglob r -> do_term r
-      | MLcons (i,r,_) -> 
-	  if lang () = Ocaml then record_iter_references do_term i; 
-	  do_cons r 
-      | MLcase (i,_,v) -> 
-	  if lang () = Ocaml then record_iter_references do_term (fst i); 
+      | MLcons (i,r,_) ->
+	  if lang () = Ocaml then record_iter_references do_term i;
+	  do_cons r
+      | MLcase (i,_,v) ->
+	  if lang () = Ocaml then record_iter_references do_term (fst i);
 	  Array.iter (fun (r,_,_) -> do_cons r) v
       | _ -> ()
   in iter a
 
-let ind_iter_references do_term do_cons do_type kn ind = 
+let ind_iter_references do_term do_cons do_type kn ind =
   let type_iter = type_iter_references do_type in
-  let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in 
-  let packet_iter ip p = 
-    do_type (IndRef ip); 
-    if lang () = Ocaml then 
-      (match ind.ind_equiv with 
-	 | Equiv kne -> do_type (IndRef (kne, snd ip)); 
-	 | _ -> ()); 
-    Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
+  let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in
+  let packet_iter ip p =
+    do_type (IndRef ip);
+    if lang () = Ocaml then
+      (match ind.ind_equiv with
+	 | Equiv kne -> do_type (IndRef (kne, snd ip));
+	 | _ -> ());
+    Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
-  if lang () = Ocaml then record_iter_references do_term ind.ind_info; 
+  if lang () = Ocaml then record_iter_references do_term ind.ind_info;
   Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
-  
-let decl_iter_references do_term do_cons do_type = 
-  let type_iter = type_iter_references do_type 
+
+let decl_iter_references do_term do_cons do_type =
+  let type_iter = type_iter_references do_type
   and ast_iter = ast_iter_references do_term do_cons do_type in
-  function 
-    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind 
-    | Dtype (r,_,t) -> do_type r; type_iter t 
+  function
+    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
+    | Dtype (r,_,t) -> do_type r; type_iter t
     | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
-    | Dfix(rv,c,t) -> 	
+    | Dfix(rv,c,t) -> 
 	Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t
 
-let spec_iter_references do_term do_cons do_type = function 
+let spec_iter_references do_term do_cons do_type = function
   | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
   | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot
   | Sval (r,t) -> do_term r; type_iter_references do_type t
@@ -127,83 +127,83 @@ let spec_iter_references do_term do_cons do_type = function
 
 exception Found
 
-let rec ast_search f a = 
+let rec ast_search f a =
   if f a then raise Found else ast_iter (ast_search f) a
 
-let decl_ast_search f = function 
+let decl_ast_search f = function
   | Dterm (_,a,_) -> ast_search f a
   | Dfix (_,c,_) -> Array.iter (ast_search f) c
-  | _ -> () 
+  | _ -> ()
 
-let struct_ast_search f s = 
+let struct_ast_search f s =
   try struct_iter (decl_ast_search f) (fun _ -> ()) s; false
   with Found -> true
 
-let rec type_search f = function  
-  | Tarr (a,b) -> type_search f a; type_search f b 
+let rec type_search f = function
+  | Tarr (a,b) -> type_search f a; type_search f b
   | Tglob (r,l) -> List.iter (type_search f) l
   | u -> if f u then raise Found
 
-let decl_type_search f = function 
-  | Dind (_,{ind_packets=p})  -> 
-      Array.iter 
+let decl_type_search f = function
+  | Dind (_,{ind_packets=p})  ->
+      Array.iter
 	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
   | Dterm (_,_,u) -> type_search f u
   | Dfix (_,_,v) -> Array.iter (type_search f) v
   | Dtype (_,_,u) -> type_search f u
 
-let spec_type_search f = function 
-  | Sind (_,{ind_packets=p}) -> 
-      Array.iter 
+let spec_type_search f = function
+  | Sind (_,{ind_packets=p}) ->
+      Array.iter
 	(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
   | Stype (_,_,ot) -> Option.iter (type_search f) ot
   | Sval (_,u) -> type_search f u
 
-let struct_type_search f s = 
+let struct_type_search f s =
   try struct_iter (decl_type_search f) (spec_type_search f) s; false
   with Found -> true
 
 
 (*s Generating the signature. *)
 
-let rec msig_of_ms = function 
-  | [] -> [] 
-  | (l,SEdecl (Dind (kn,i))) :: ms -> 
+let rec msig_of_ms = function
+  | [] -> []
+  | (l,SEdecl (Dind (kn,i))) :: ms ->
       (l,Spec (Sind (kn,i))) :: (msig_of_ms ms)
-  | (l,SEdecl (Dterm (r,_,t))) :: ms -> 
+  | (l,SEdecl (Dterm (r,_,t))) :: ms ->
       (l,Spec (Sval (r,t))) :: (msig_of_ms ms)
-  | (l,SEdecl (Dtype (r,v,t))) :: ms -> 
-      (l,Spec (Stype (r,v,Some t))) :: (msig_of_ms ms) 
-  | (l,SEdecl (Dfix (rv,_,tv))) :: ms -> 
-      let msig = ref (msig_of_ms ms) in 
-      for i = Array.length rv - 1 downto 0 do 
+  | (l,SEdecl (Dtype (r,v,t))) :: ms ->
+      (l,Spec (Stype (r,v,Some t))) :: (msig_of_ms ms)
+  | (l,SEdecl (Dfix (rv,_,tv))) :: ms ->
+      let msig = ref (msig_of_ms ms) in
+      for i = Array.length rv - 1 downto 0 do
 	msig := (l,Spec (Sval (rv.(i),tv.(i))))::!msig
-      done; 
+      done;
       !msig
   | (l,SEmodule m) :: ms -> (l,Smodule m.ml_mod_type) :: (msig_of_ms ms)
   | (l,SEmodtype m) :: ms -> (l,Smodtype m) :: (msig_of_ms ms)
 
-let signature_of_structure s = 
-  List.map (fun (mp,ms) -> mp,msig_of_ms ms) s 
+let signature_of_structure s =
+  List.map (fun (mp,ms) -> mp,msig_of_ms ms) s
 
 
 (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)
 
-let get_decl_in_structure r struc = 
-  try 
-    let base_mp,ll = labels_of_ref r in 
+let get_decl_in_structure r struc =
+  try
+    let base_mp,ll = labels_of_ref r in
     if not (at_toplevel base_mp) then error_not_visible r;
     let sel = List.assoc base_mp struc in
-    let rec go ll sel = match ll with 
+    let rec go ll sel = match ll with
       | [] -> assert false
-      | l :: ll -> 
-	  match List.assoc l sel with 
-	    | SEdecl d -> d 
+      | l :: ll ->
+	  match List.assoc l sel with
+	    | SEdecl d -> d
 	    | SEmodtype m -> assert false
 	    | SEmodule m ->
-		match m.ml_mod_expr with 
-		  | MEstruct (_,sel) -> go ll sel 
-		  | _ -> error_not_visible r 
+		match m.ml_mod_expr with
+		  | MEstruct (_,sel) -> go ll sel
+		  | _ -> error_not_visible r
     in go ll sel
   with Not_found -> assert false
 
@@ -216,83 +216,83 @@ let get_decl_in_structure r struc =
    a let-in redex is created for clarity) and iota redexes, plus some other
    optimizations. *)
 
-let dfix_to_mlfix rv av i = 
-  let rec make_subst n s = 
-    if n < 0 then s 
+let dfix_to_mlfix rv av i =
+  let rec make_subst n s =
+    if n < 0 then s
     else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
-  in 
-  let s = make_subst (Array.length rv - 1) Refmap.empty 
-  in 
-  let rec subst n t = match t with 
-    | MLglob ((ConstRef kn) as refe) -> 
+  in
+  let s = make_subst (Array.length rv - 1) Refmap.empty
+  in
+  let rec subst n t = match t with
+    | MLglob ((ConstRef kn) as refe) ->
 	(try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
-    | _ -> ast_map_lift subst n t 
-  in 
-  let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in 
-  let c = Array.map (subst 0) av 
+    | _ -> ast_map_lift subst n t
+  in
+  let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in
+  let c = Array.map (subst 0) av
   in MLfix(i, ids, c)
 
 let rec optim to_appear s = function
   | [] -> []
   | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
-      if List.mem r to_appear 
-      then d :: (optim to_appear s l) 
+      if List.mem r to_appear
+      then d :: (optim to_appear s l)
       else optim to_appear s l
   | Dterm (r,t,typ) :: l ->
-      let t = normalize (ast_glob_subst !s t) in 
-      let i = inline r t in 
-      if i then s := Refmap.add r t !s; 
-      if not i || modular () || List.mem r to_appear 
-      then 
-	let d = match optimize_fix t with 
-	  | MLfix (0, _, [|c|]) -> 
+      let t = normalize (ast_glob_subst !s t) in
+      let i = inline r t in
+      if i then s := Refmap.add r t !s;
+      if not i || modular () || List.mem r to_appear
+      then
+	let d = match optimize_fix t with
+	  | MLfix (0, _, [|c|]) ->
 	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|])
 	  | t -> Dterm (r, t, typ)
 	in d :: (optim to_appear s l)
       else optim to_appear s l
   | d :: l -> d :: (optim to_appear s l)
 
-let rec optim_se top to_appear s = function 
-  | [] -> [] 
-  | (l,SEdecl (Dterm (r,a,t))) :: lse -> 
-      let a = normalize (ast_glob_subst !s a) in 
-      let i = inline r a in 
-      if i then s := Refmap.add r a !s; 
+let rec optim_se top to_appear s = function
+  | [] -> []
+  | (l,SEdecl (Dterm (r,a,t))) :: lse ->
+      let a = normalize (ast_glob_subst !s a) in
+      let i = inline r a in
+      if i then s := Refmap.add r a !s;
       if top && i && not (modular ()) && not (List.mem r to_appear)
       then optim_se top to_appear s lse
-      else 
-	let d = match optimize_fix a with 
-	  | MLfix (0, _, [|c|]) -> 
+      else
+	let d = match optimize_fix a with
+	  | MLfix (0, _, [|c|]) ->
 	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
 	  | a -> Dterm (r, a, t)
 	in (l,SEdecl d) :: (optim_se top to_appear s lse)
-  | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> 
-      let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in 
-      let all = ref true in 
+  | (l,SEdecl (Dfix (rv,av,tv))) :: lse ->
+      let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in
+      let all = ref true in
       (* This fake body ensures that no fixpoint will be auto-inlined. *)
-      let fake_body = MLfix (0,[||],[||]) in 
-      for i = 0 to Array.length rv - 1 do 
+      let fake_body = MLfix (0,[||],[||]) in
+      for i = 0 to Array.length rv - 1 do
 	if inline rv.(i) fake_body
 	then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
 	else all := false
-      done; 
+      done;
       if !all && top && not (modular ())
-	&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)  
+	&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)
       then optim_se top to_appear s lse
       else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
-  | (l,SEmodule m) :: lse -> 
+  | (l,SEmodule m) :: lse ->
       let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
       in (l,SEmodule m) :: (optim_se top to_appear s lse)
-  | se :: lse -> se :: (optim_se top to_appear s lse) 
+  | se :: lse -> se :: (optim_se top to_appear s lse)
 
-and optim_me to_appear s = function 
+and optim_me to_appear s = function
   | MEstruct (msid, lse) -> MEstruct (msid, optim_se false to_appear s lse)
   | MEident mp as me -> me
-  | MEapply (me, me') -> 
+  | MEapply (me, me') ->
       MEapply (optim_me to_appear s me, optim_me to_appear s me')
   | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me)
 
-(* After these optimisations, some dependencies may not be needed anymore. 
+(* After these optimisations, some dependencies may not be needed anymore.
    For monolithic extraction, we recompute a minimal set of dependencies. *)
 
 exception NoDepCheck
@@ -316,7 +316,7 @@ let declared_refs = function
   | Dterm (r,_,_) -> [|r|]
   | Dfix (rv,_,_) -> rv
 
-(* Computes the dependencies of a declaration, except in case 
+(* Computes the dependencies of a declaration, except in case
    of custom extraction. *)
 
 let compute_deps_decl = function
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index fdb58e631..8e04a368e 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -20,7 +20,7 @@ open Mod_subst
 val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
 val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
 
-type do_ref = global_reference -> unit 
+type do_ref = global_reference -> unit
 
 val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
 val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 55fa78c55..93fc2c2dc 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -25,16 +25,16 @@ open Declarations
 
 (*s Some utility functions. *)
 
-let pp_tvar id = 
-  let s = string_of_id id in 
-  if String.length s < 2 || s.[1]<>'\'' 
+let pp_tvar id =
+  let s = string_of_id id in
+  if String.length s < 2 || s.[1]<>'\''
   then str ("'"^s)
   else str ("' "^s)
 
 let pp_tuple_light f = function
   | [] -> mt ()
   | [x] -> f true x
-  | l -> 
+  | l ->
       pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
 
 let pp_tuple f = function
@@ -49,19 +49,19 @@ let pp_boxed_tuple f = function
 
 let pp_abst = function
   | [] -> mt ()
-  | l  -> 
-      str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ 
+  | l  ->
+      str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
       str " ->" ++ spc ()
 
-let pp_parameters l = 
+let pp_parameters l =
   (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
 
-let pp_string_parameters l = 
-  (pp_boxed_tuple str l ++ space_if (l<>[])) 
+let pp_string_parameters l =
+  (pp_boxed_tuple str l ++ space_if (l<>[]))
 
 (*s Ocaml renaming issues. *)
 
-let keywords =     
+let keywords =
   List.fold_right (fun s -> Idset.add (id_of_string s))
   [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
     "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
@@ -70,16 +70,16 @@ let keywords =
     "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
-    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] 
+    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
   Idset.empty
 
 let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
 
-let preamble _ used_modules usf = 
+let preamble _ used_modules usf =
   prlist pp_open used_modules ++
   (if used_modules = [] then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
-  (if usf.mldummy then 
+  (if usf.mldummy then
      str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n"
    else mt ()) ++
   (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
@@ -92,8 +92,8 @@ let sig_preamble _ used_modules usf =
 (*s The pretty-printer for Ocaml syntax*)
 
 (* Beware of the side-effects of [pp_global] and [pp_modname].
-   They are used to update table of content for modules. Many [let] 
-   below should not be altered since they force evaluation order. 
+   They are used to update table of content for modules. Many [let]
+   below should not be altered since they force evaluation order.
 *)
 
 let pp_global k r =
@@ -103,14 +103,14 @@ let pp_global k r =
 let pp_modname mp = str (Common.pp_module mp)
 
 
-let is_infix r = 
-  is_inline_custom r && 
-  (let s = find_custom r in 
-   let l = String.length s in 
+let is_infix r =
+  is_inline_custom r &&
+  (let s = find_custom r in
+   let l = String.length s in
    l >= 2 && s.[0] = '(' && s.[l-1] = ')')
 
-let get_infix r = 
-  let s = find_custom r in 
+let get_infix r =
+  let s = find_custom r in
   String.sub s 1 (String.length s - 2)
 
 exception NoRecord
@@ -120,31 +120,31 @@ let find_projections = function Record l -> l | _ -> raise NoRecord
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let kn_sig = 
-  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in 
+let kn_sig =
+  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
   make_kn specif empty_dirpath (mk_label "sig")
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
-    | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
+    | Tvar i -> (try pp_tvar (List.nth vl (pred i))
 		 with _ -> (str "'a" ++ int i))
-    | Tglob (r,[a1;a2]) when is_infix r -> 
-	pp_par par 
-	  (pp_rec true a1 ++ spc () ++ str (get_infix r) ++ spc () ++ 
+    | Tglob (r,[a1;a2]) when is_infix r ->
+	pp_par par
+	  (pp_rec true a1 ++ spc () ++ str (get_infix r) ++ spc () ++
 	   pp_rec true a2)
     | Tglob (r,[]) -> pp_global Type r
-    | Tglob (r,l) -> 
-	if r = IndRef (kn_sig,0) then 
+    | Tglob (r,l) ->
+	if r = IndRef (kn_sig,0) then
 	  pp_tuple_light pp_rec l
-	else 
+	else
 	  pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
     | Tarr (t1,t2) ->
-	pp_par par 
+	pp_par par
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy _ -> str "__"
     | Tunknown -> str "__"
-  in 
+  in
   hov 0 (pp_rec par t)
 
 (*s Pretty-printing of expressions. [par] indicates whether
@@ -152,29 +152,29 @@ let rec pp_type par vl t =
     de Bruijn variables. [args] is the list of collected arguments
     (already pretty-printed). *)
 
-let is_ifthenelse = function 
-  | [|(r1,[],_);(r2,[],_)|] -> 
-      (try (find_custom r1 = "true") && (find_custom r2 = "false") 
+let is_ifthenelse = function
+  | [|(r1,[],_);(r2,[],_)|] ->
+      (try (find_custom r1 = "true") && (find_custom r2 = "false")
        with Not_found -> false)
   | _ -> false
 
 let expr_needs_par = function
   | MLlam _  -> true
-  | MLcase (_,_,[|_|]) -> false 
+  | MLcase (_,_,[|_|]) -> false
   | MLcase (_,_,pv) -> not (is_ifthenelse pv)
-  | _        -> false 
+  | _        -> false
 
 
-let rec pp_expr par env args = 
+let rec pp_expr par env args =
   let par' = args <> [] || par
-  and apply st = pp_apply st par args in 
+  and apply st = pp_apply st par args in
   function
-    | MLrel n -> 
+    | MLrel n ->
 	let id = get_db_name n env in apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
-    | MLlam _ as a -> 
+    | MLlam _ as a ->
       	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
 	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
@@ -183,159 +183,159 @@ let rec pp_expr par env args =
 	let i,env' = push_vars [id] env in
 	let pp_id = pr_id (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
-	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in 
-	hv 0 
-	  (apply 
-	     (pp_par par' 
-		(hv 0 
-		   (hov 2 
-		      (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++ 
-		    spc () ++ str "in") ++ 
+	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
+	hv 0
+	  (apply
+	     (pp_par par'
+		(hv 0
+		   (hov 2
+		      (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++
+		    spc () ++ str "in") ++
 		 spc () ++ hov 0 pp_a2)))
-    | MLglob r -> 
-	(try 
-	   let args = list_skipn (projection_arity r) args in 
-	   let record = List.hd args in 
+    | MLglob r ->
+	(try
+	   let args = list_skipn (projection_arity r) args in
+	   let record = List.hd args in
 	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
 	 with _ -> apply (pp_global Term r))
     | MLcons (Coinductive,r,[]) ->
 	assert (args=[]);
 	pp_par par (str "lazy " ++ pp_global Cons r)
-    | MLcons (Coinductive,r,args') -> 
+    | MLcons (Coinductive,r,args') ->
 	assert (args=[]);
-	let tuple = pp_tuple (pp_expr true env []) args' in 
+	let tuple = pp_tuple (pp_expr true env []) args' in
 	pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
-    | MLcons (_,r,[]) -> 
+    | MLcons (_,r,[]) ->
 	assert (args=[]);
 	pp_global Cons r
-    | MLcons (Record projs, r, args') -> 
-	assert (args=[]); 
+    | MLcons (Record projs, r, args') ->
+	assert (args=[]);
 	pp_record_pat (projs, List.map (pp_expr true env []) args')
-    | MLcons (_,r,[arg1;arg2]) when is_infix r -> 
-	assert (args=[]); 
+    | MLcons (_,r,[arg1;arg2]) when is_infix r ->
+	assert (args=[]);
 	pp_par par
 	  ((pp_expr true env [] arg1) ++ spc () ++ str (get_infix r) ++
 	   spc () ++ (pp_expr true env [] arg2))
-    | MLcons (_,r,args') -> 
+    | MLcons (_,r,args') ->
 	assert (args=[]);
-	let tuple = pp_tuple (pp_expr true env []) args' in 
+	let tuple = pp_tuple (pp_expr true env []) args' in
 	pp_par par (pp_global Cons r ++ spc () ++ tuple)
     | MLcase ((i,factors), t, pv) ->
-	let expr = if i = Coinductive then 
+	let expr = if i = Coinductive then
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
-	else 
-	  (pp_expr false env [] t) 
-	in 
-	(try 
-	   let projs = find_projections i in 
-	   let (_, ids, c) = pv.(0) in 
-	   let n = List.length ids in 
-	   match c with 
-	     | MLrel i when i <= n -> 
-		 apply (pp_par par' (pp_expr true env [] t ++ str "." ++ 
+	else
+	  (pp_expr false env [] t)
+	in
+	(try
+	   let projs = find_projections i in
+	   let (_, ids, c) = pv.(0) in
+	   let n = List.length ids in
+	   match c with
+	     | MLrel i when i <= n ->
+		 apply (pp_par par' (pp_expr true env [] t ++ str "." ++
 				     pp_global Term (List.nth projs (n-i))))
-	     | MLapp (MLrel i, a) when i <= n -> 
-		 if List.exists (ast_occurs_itvl 1 n) a 
+	     | MLapp (MLrel i, a) when i <= n ->
+		 if List.exists (ast_occurs_itvl 1 n) a
 		 then raise NoRecord
 		 else
 		   let ids,env' = push_vars (List.rev ids) env in
-		   (pp_apply 
-		      (pp_expr true env [] t ++ str "." ++ 
+		   (pp_apply
+		      (pp_expr true env [] t ++ str "." ++
 		       pp_global Term (List.nth projs (n-i)))
 		      par ((List.map (pp_expr true env' []) a) @ args))
 	     | _ -> raise NoRecord
-	 with NoRecord -> 
-	   if Array.length pv = 1 then 
-	     let s1,s2 = pp_one_pat env i pv.(0) in 
-	     apply 
-	       (hv 0 
-		  (pp_par par' 
-		     (hv 0 
-			(hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) 
-			 ++ spc () ++ str "in") ++ 
+	 with NoRecord ->
+	   if Array.length pv = 1 then
+	     let s1,s2 = pp_one_pat env i pv.(0) in
+	     apply
+	       (hv 0
+		  (pp_par par'
+		     (hv 0
+			(hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr)
+			 ++ spc () ++ str "in") ++
 		      spc () ++ hov 0 s2)))
-	   else 
+	   else
  	     apply
-      	       (pp_par par' 
-		  (try pp_ifthenelse par' env expr pv 
-		   with Not_found -> 
+      	       (pp_par par'
+		  (try pp_ifthenelse par' env expr pv
+		   with Not_found ->
 		     v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
 			  str "  | " ++ pp_pat env (i,factors) pv))))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
-    | MLexn s -> 
+    | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLmagic a ->
 	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
-    | MLaxiom -> 
+    | MLaxiom ->
 	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
 
-	  
+
 and pp_record_pat (projs, args) =
    str "{ " ++
-   prlist_with_sep (fun () -> str ";" ++ spc ()) 
+   prlist_with_sep (fun () -> str ";" ++ spc ())
      (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a)
      (List.combine projs args) ++
    str " }"
 
-and pp_ifthenelse par env expr pv = match pv with 
-  | [|(tru,[],the);(fal,[],els)|] when 
+and pp_ifthenelse par env expr pv = match pv with
+  | [|(tru,[],the);(fal,[],els)|] when
       (find_custom tru = "true") && (find_custom fal = "false")
-      -> 
-      hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++ 
+      ->
+      hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
             hov 2 (str "then " ++
-		   hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++ 
+		   hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++
 	    hov 2 (str "else " ++
 	           hov 2 (pp_expr (expr_needs_par els) env [] els)))
   | _ -> raise Not_found
 
-and pp_one_pat env i (r,ids,t) = 
+and pp_one_pat env i (r,ids,t) =
   let ids,env' = push_vars (List.rev ids) env in
-  let expr = pp_expr (expr_needs_par t) env' [] t in 
-  try 
-    let projs = find_projections i in 
+  let expr = pp_expr (expr_needs_par t) env' [] t in
+  try
+    let projs = find_projections i in
     pp_record_pat (projs, List.rev_map pr_id ids), expr
-  with NoRecord -> 
-    (match List.rev ids with 
-      | [i1;i2] when is_infix r -> 
+  with NoRecord ->
+    (match List.rev ids with
+      | [i1;i2] when is_infix r ->
 	  pr_id i1 ++ str " " ++ str (get_infix r) ++ str " " ++ pr_id i2
       | [] -> pp_global Cons r
-      | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids), 
+      | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids),
     expr
-  
-and pp_pat env (info,factors) pv = 
-  prvecti 
-    (fun i x -> if List.mem i factors then mt () else 
-       let s1,s2 = pp_one_pat env info x in 
+
+and pp_pat env (info,factors) pv =
+  prvecti
+    (fun i x -> if List.mem i factors then mt () else
+       let s1,s2 = pp_one_pat env info x in
        hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
-       (if factors = [] && i = Array.length pv-1 then mt () 
-	else fnl () ++ str "  | ")) pv 
-  ++ 
-  match factors with 
+       (if factors = [] && i = Array.length pv-1 then mt ()
+	else fnl () ++ str "  | ")) pv
+  ++
+  match factors with
      | [] -> mt ()
-     | i::_ -> 
-	 let (_,ids,t) = pv.(i) in 
-	 let t = ast_lift (-List.length ids) t in 
+     | i::_ ->
+	 let (_,ids,t) = pv.(i) in
+	 let t = ast_lift (-List.length ids) t in
 	 hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t)
 
 and pp_function env t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars bl env in
-  match t' with 
-    | MLcase(i,MLrel 1,pv) when fst i=Standard -> 
-	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then 
+  match t' with
+    | MLcase(i,MLrel 1,pv) when fst i=Standard ->
+	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
        	  str " = function" ++ fnl () ++
 	  v 0 (str "  | " ++ pp_pat env' i pv)
 	else
-          pr_binding (List.rev bl) ++ 
+          pr_binding (List.rev bl) ++
           str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
 	  v 0 (str "  | " ++ pp_pat env' i pv)
-    | _ -> 
+    | _ ->
           pr_binding (List.rev bl) ++
 	  str " =" ++ fnl () ++ str "  " ++
 	  hov 2 (pp_expr false env' [] t')
@@ -344,7 +344,7 @@ and pp_function env t =
     and passed here just for convenience. *)
 
 and pp_fix par env i (ids,bl) args =
-  pp_par par 
+  pp_par par
     (v 0 (str "let rec " ++
 	  prvect_with_sep
       	    (fun () -> fnl () ++ str "and ")
@@ -353,33 +353,33 @@ and pp_fix par env i (ids,bl) args =
 	  fnl () ++
 	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 
-let pp_val e typ = 
-  hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ 
+let pp_val e typ =
+  hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++
   str " **)")  ++ fnl2 ()
 
 (*s Pretty-printing of [Dfix] *)
 
-let pp_Dfix (rv,c,t) = 
-  let names = Array.map 
+let pp_Dfix (rv,c,t) =
+  let names = Array.map
     (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
-  in 
-  let rec pp sep letand i = 
+  in
+  let rec pp sep letand i =
     if i >= Array.length rv then mt ()
     else if is_inline_custom rv.(i) then pp sep letand (i+1)
-    else 
-      let def = 
+    else
+      let def =
 	if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
 	else pp_function (empty_env ()) c.(i)
-      in 
-      sep () ++ pp_val names.(i) t.(i) ++ 
-      str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1) 
+      in
+      sep () ++ pp_val names.(i) t.(i) ++
+      str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1)
   in pp mt "let rec " 0
 
 (*s Pretty-printing of inductive types declaration. *)
 
-let pp_equiv param_list name = function 
+let pp_equiv param_list name = function
   | NoEquiv, _ -> mt ()
-  | Equiv kn, i -> 
+  | Equiv kn, i ->
       str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i))
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
@@ -389,97 +389,97 @@ let pp_comment s = str "(* " ++ s ++ str " *)"
 let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   let pl = rename_tvars keywords pl in
   let pp_constructor i typs =
-    (if i=0 then mt () else fnl ()) ++ 
+    (if i=0 then mt () else fnl ()) ++
     hov 5 (str "  | " ++ cnames.(i) ++
 	   (if typs = [] then mt () else str " of ") ++
-	   prlist_with_sep 
+	   prlist_with_sep
 	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
   in
   pp_parameters pl ++ str prefix ++ name ++
   pp_equiv pl name ip_equiv ++ str " =" ++
-  if Array.length ctyps = 0 then str " unit (* empty inductive *)" 
+  if Array.length ctyps = 0 then str " unit (* empty inductive *)"
   else fnl () ++ v 0 (prvecti pp_constructor ctyps)
 
-let pp_logical_ind packet = 
-  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ 
+let pp_logical_ind packet =
+  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
   fnl () ++
-  pp_comment (str "with constructors : " ++ 
+  pp_comment (str "with constructors : " ++
 	      prvect_with_sep spc pr_id packet.ip_consnames) ++
   fnl ()
 
-let pp_singleton kn packet = 
-  let name = pp_global Type (IndRef (kn,0)) in 
-  let l = rename_tvars keywords packet.ip_vars in 
+let pp_singleton kn packet =
+  let name = pp_global Type (IndRef (kn,0)) in
+  let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment (str "singleton inductive, whose constructor was " ++ 
+	 pp_comment (str "singleton inductive, whose constructor was " ++
 		     pr_id packet.ip_consnames.(0)))
 
-let pp_record kn projs ip_equiv packet = 
+let pp_record kn projs ip_equiv packet =
   let name = pp_global Type (IndRef (kn,0)) in
-  let projnames = List.map (pp_global Term) projs in 
-  let l = List.combine projnames packet.ip_types.(0) in 
-  let pl = rename_tvars keywords packet.ip_vars in 
-  str "type " ++ pp_parameters pl ++ name ++ 
+  let projnames = List.map (pp_global Term) projs in
+  let l = List.combine projnames packet.ip_types.(0) in
+  let pl = rename_tvars keywords packet.ip_vars in
+  str "type " ++ pp_parameters pl ++ name ++
   pp_equiv pl name ip_equiv ++ str " = { "++
-  hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
-	   (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l) 
+  hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ())
+	   (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l)
   ++ str " }"
 
-let pp_coind pl name = 
+let pp_coind pl name =
   let pl = rename_tvars keywords pl in
-  pp_parameters pl ++ name ++ str " = " ++ 
-  pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++ 
+  pp_parameters pl ++ name ++ str " = " ++
+  pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++
   fnl() ++ str "and "
 
 let pp_ind co kn ind =
-  let prefix = if co then "__" else "" in 
-  let some = ref false in 
-  let init= ref (str "type ") in 
-  let names = 
-    Array.mapi (fun i p -> if p.ip_logical then mt () else 
+  let prefix = if co then "__" else "" in
+  let some = ref false in
+  let init= ref (str "type ") in
+  let names =
+    Array.mapi (fun i p -> if p.ip_logical then mt () else
 		  pp_global Type (IndRef (kn,i)))
       ind.ind_packets
-  in 
-  let cnames = 
-    Array.mapi 
-      (fun i p -> if p.ip_logical then [||] else 
+  in
+  let cnames =
+    Array.mapi
+      (fun i p -> if p.ip_logical then [||] else
 	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1)))
 	   p.ip_types)
       ind.ind_packets
-  in 
-  let rec pp i =  
-    if i >= Array.length ind.ind_packets then mt () 
-    else 
-      let ip = (kn,i) in 
-      let ip_equiv = ind.ind_equiv, i in 
-      let p = ind.ind_packets.(i) in 
+  in
+  let rec pp i =
+    if i >= Array.length ind.ind_packets then mt ()
+    else
+      let ip = (kn,i) in
+      let ip_equiv = ind.ind_equiv, i in
+      let p = ind.ind_packets.(i) in
       if is_custom (IndRef ip) then pp (i+1)
-      else begin 
-	some := true; 
+      else begin
+	some := true;
 	if p.ip_logical then pp_logical_ind p ++ pp (i+1)
-	else 
-	  let s = !init in 
-	  begin 
-	    init := (fnl () ++ str "and "); 
+	else
+	  let s = !init in
+	  begin
+	    init := (fnl () ++ str "and ");
 	    s ++
 	    (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
-	    pp_one_ind 
+	    pp_one_ind
 	      prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
 	    pp (i+1)
 	  end
       end
-  in 
+  in
   let st = pp 0 in if !some then st else failwith "empty phrase"
-	     
+
 
 (*s Pretty-printing of a declaration. *)
 
-let pp_mind kn i = 
-  match i.ind_info with 
+let pp_mind kn i =
+  match i.ind_info with
     | Singleton -> pp_singleton kn i.ind_packets.(0)
     | Coinductive -> pp_ind true kn i
-    | Record projs -> 
+    | Record projs ->
 	pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0)
     | Standard -> pp_ind false kn i
 
@@ -487,119 +487,119 @@ let pp_decl = function
     | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
     | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"
     | Dind (kn,i) -> pp_mind kn i
-    | Dtype (r, l, t) -> 
-        let name = pp_global Type r in 
-	let l = rename_tvars keywords l in 
-        let ids, def = 
-	  try 
-	    let ids,s = find_type_custom r in 
-	    pp_string_parameters ids, str "=" ++ spc () ++ str s 
-	  with Not_found -> 
-	    pp_parameters l, 
+    | Dtype (r, l, t) ->
+        let name = pp_global Type r in
+	let l = rename_tvars keywords l in
+        let ids, def =
+	  try
+	    let ids,s = find_type_custom r in
+	    pp_string_parameters ids, str "=" ++ spc () ++ str s
+	  with Not_found ->
+	    pp_parameters l,
 	    if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
 	    else str "=" ++ spc () ++ pp_type false l t
-	in 
+	in
 	hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
-    | Dterm (r, a, t) -> 
-	let def = 
+    | Dterm (r, a, t) ->
+	let def =
 	  if is_custom r then str (" = " ^ find_custom r)
-	  else if is_projection r then 
-	    (prvect str (Array.make (projection_arity r) " _")) ++ 
+	  else if is_projection r then
+	    (prvect str (Array.make (projection_arity r) " _")) ++
 	    str " x = x."
 	  else pp_function (empty_env ()) a
-	in 
-	let name = pp_global Term r in 
-	let postdef = if is_projection r then name else mt () in 
+	in
+	let name = pp_global Term r in
+	let postdef = if is_projection r then name else mt () in
 	pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef)
     | Dfix (rv,defs,typs) ->
 	pp_Dfix (rv,defs,typs)
 
-let pp_alias_decl ren = function 
+let pp_alias_decl ren = function
   | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Dtype (r, l, _) -> 
-      let name = pp_global Type r in 
-      let l = rename_tvars keywords l in 
-      let ids = pp_parameters l in 
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ 
+  | Dtype (r, l, _) ->
+      let name = pp_global Type r in
+      let l = rename_tvars keywords l in
+      let ids = pp_parameters l in
+      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
 	     str (ren^".") ++ name)
-  | Dterm (r, a, t) -> 
+  | Dterm (r, a, t) ->
       let name = pp_global Term r in
       hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
   | Dfix (rv, _, _) ->
-      prvecti (fun i r -> if is_inline_custom r then mt () else 
-		 let name = pp_global Term r in 
+      prvecti (fun i r -> if is_inline_custom r then mt () else
+		 let name = pp_global Term r in
 		 hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
-		 fnl ()) 
+		 fnl ())
 	rv
 
-let pp_spec = function 
+let pp_spec = function
   | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
   | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
   | Sind (kn,i) -> pp_mind kn i
-  | Sval (r,t) -> 
-      let def = pp_type false [] t in 
-      let name = pp_global Term r in 
+  | Sval (r,t) ->
+      let def = pp_type false [] t in
+      let name = pp_global Term r in
       hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
-  | Stype (r,vl,ot) -> 
+  | Stype (r,vl,ot) ->
       let name = pp_global Type r in
-      let l = rename_tvars keywords vl in 
-      let ids, def = 
-	try 
-	  let ids, s = find_type_custom r in 
-	  pp_string_parameters ids,  str "= " ++ str s 
-	with Not_found -> 
-	  let ids = pp_parameters l in 
-	  match ot with 
+      let l = rename_tvars keywords vl in
+      let ids, def =
+	try
+	  let ids, s = find_type_custom r in
+	  pp_string_parameters ids,  str "= " ++ str s
+	with Not_found ->
+	  let ids = pp_parameters l in
+	  match ot with
 	    | None -> ids, mt ()
-	    | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" 
-	    | Some t -> ids, str "=" ++ spc () ++ pp_type false l t 
-      in 
+	    | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)"
+	    | Some t -> ids, str "=" ++ spc () ++ pp_type false l t
+      in
       hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
 
-let pp_alias_spec ren = function 
+let pp_alias_spec ren = function
   | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Stype (r,l,_) ->       
-      let name = pp_global Type r in 
-      let l = rename_tvars keywords l in 
-      let ids = pp_parameters l in 
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ 
+  | Stype (r,l,_) ->
+      let name = pp_global Type r in
+      let l = rename_tvars keywords l in
+      let ids = pp_parameters l in
+      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
 	     str (ren^".") ++ name)
   | Sval _ -> assert false
-	  
-let rec pp_specif = function 
+
+let rec pp_specif = function
   | (_,Spec (Sval _ as s)) -> pp_spec s
-  | (l,Spec s) -> 
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+  | (l,Spec s) ->
+      (try
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in
 	 hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++
 	 fnl () ++ str "end" ++ fnl () ++
 	 pp_alias_spec ren s
        with Not_found -> pp_spec s)
-  | (l,Smodule mt) -> 
-      let def = pp_module_type (Some l) mt in 
-      let def' = pp_module_type (Some l) mt in 
-      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
+  | (l,Smodule mt) ->
+      let def = pp_module_type (Some l) mt in
+      let def' = pp_module_type (Some l) mt in
+      let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
-      (try 
+      (try
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in
 	 fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
        with Not_found -> Pp.mt ())
-  | (l,Smodtype mt) -> 
-      let def = pp_module_type None mt in 
+  | (l,Smodtype mt) ->
+      let def = pp_module_type None mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+      (try
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in
 	 fnl () ++ str ("module type "^ren^" = ") ++ name
        with Not_found -> Pp.mt ())
 
-and pp_module_type ol = function 
-  | MTident kn -> 
+and pp_module_type ol = function
+  | MTident kn ->
       pp_modname kn
-  | MTfunsig (mbid, mt, mt') -> 
-      let typ = pp_module_type None mt in 
-      let name = pp_modname (MPbound mbid) in 
-      let def = pp_module_type None mt' in 
+  | MTfunsig (mbid, mt, mt') ->
+      let typ = pp_module_type None mt in
+      let name = pp_modname (MPbound mbid) in
+      let def = pp_module_type None mt' in
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (msid, sign) ->
       let tvm = top_visible_mp () in
@@ -607,9 +607,9 @@ and pp_module_type ol = function
       (* References in [sign] are in short form (relative to [msid]).
 	 In push_visible, [msid-->mp] is added to the current subst. *)
       push_visible mp (Some msid);
-      let l = map_succeed pp_specif sign in 
-      pop_visible (); 
-      str "sig " ++ fnl () ++ 
+      let l = map_succeed pp_specif sign in
+      pop_visible ();
+      str "sig " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
 	fnl () ++ str "end"
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
@@ -641,14 +641,14 @@ and pp_module_type ol = function
       s ++ str " = " ++ pp_modname mp
 
 let is_short = function MEident _ | MEapply _ -> true | _ -> false
-  
-let rec pp_structure_elem = function 
-  | (l,SEdecl d) -> 
-       (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+
+let rec pp_structure_elem = function
+  | (l,SEdecl d) ->
+       (try
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in
 	 hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_decl ren d 
+	 pp_alias_decl ren d
 	with Not_found -> pp_decl d)
   | (l,SEmodule m) ->
       let typ =
@@ -657,44 +657,44 @@ let rec pp_structure_elem = function
 	  str ": " ++ pp_module_type (Some l) m.ml_mod_type
 	else mt ()
       in
-      let def = pp_module_expr (Some l) m.ml_mod_expr in 
-      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
-      hov 1 
-	(str "module " ++ name ++ typ ++ str " = " ++ 
-	 (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ 
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+      let def = pp_module_expr (Some l) m.ml_mod_expr in
+      let name = pp_modname (MPdot (top_visible_mp (), l)) in
+      hov 1
+	(str "module " ++ name ++ typ ++ str " = " ++
+	 (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++
+      (try
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in
 	 fnl () ++ str ("module "^ren^" = ") ++ name
        with Not_found -> mt ())
-  | (l,SEmodtype m) -> 
-      let def = pp_module_type None m in 
-      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
+  | (l,SEmodtype m) ->
+      let def = pp_module_type None m in
+      let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
-      (try 
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+      (try
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in
          fnl () ++ str ("module type "^ren^" = ") ++ name
        with Not_found -> mt ())
 
-and pp_module_expr ol = function 
+and pp_module_expr ol = function
   | MEident mp' -> pp_modname mp'
-  | MEfunctor (mbid, mt, me) -> 
+  | MEfunctor (mbid, mt, me) ->
       let name = pp_modname (MPbound mbid) in
-      let typ = pp_module_type None mt in 
-      let def = pp_module_expr None me in 
+      let typ = pp_module_type None mt in
+      let def = pp_module_expr None me in
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
-  | MEapply (me, me') -> 
+  | MEapply (me, me') ->
       pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")"
-  | MEstruct (msid, sel) -> 
-      let tvm = top_visible_mp () in 
+  | MEstruct (msid, sel) ->
+      let tvm = top_visible_mp () in
       let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
       (* No need to update the subst with [Some msid] below : names are
 	 already in long form (see [subst_structure] in [Extract_env]). *)
-      push_visible mp None; 
-      let l = map_succeed pp_structure_elem sel in 
-      pop_visible (); 
+      push_visible mp None;
+      let l = map_succeed pp_structure_elem sel in
+      pop_visible ();
       str "struct " ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ 
-      fnl () ++ str "end" 
+      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
+      fnl () ++ str "end"
 
 let do_struct f s =
   let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
@@ -717,15 +717,15 @@ let pp_signature s = do_struct pp_specif s
 let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
 
 let ocaml_descr = {
-  keywords = keywords;  
-  file_suffix = ".ml"; 
-  capital_file = false;  
-  preamble = preamble; 
-  pp_struct = pp_struct; 
-  sig_suffix = Some ".mli";  
-  sig_preamble = sig_preamble; 
+  keywords = keywords;
+  file_suffix = ".ml";
+  capital_file = false;
+  preamble = preamble;
+  pp_struct = pp_struct;
+  sig_suffix = Some ".mli";
+  sig_preamble = sig_preamble;
   pp_sig = pp_signature;
-  pp_decl = pp_decl; 
+  pp_decl = pp_decl;
 }
 
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index c127fc1d1..4a1c1778f 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -8,5 +8,5 @@
 
 (*i $Id$ i*)
 
-val ocaml_descr : Miniml.language_descr 
+val ocaml_descr : Miniml.language_descr
 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 75af1b7bc..eaa47f5f9 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -22,38 +22,38 @@ open Common
 
 (*s Scheme renaming issues. *)
 
-let keywords =     
+let keywords =
   List.fold_right (fun s -> Idset.add (id_of_string s))
-    [ "define"; "let"; "lambda"; "lambdas"; "match"; 
-      "apply"; "car"; "cdr"; 
-      "error"; "delay"; "force"; "_"; "__"] 
+    [ "define"; "let"; "lambda"; "lambdas"; "match";
+      "apply"; "car"; "cdr";
+      "error"; "delay"; "force"; "_"; "__"]
     Idset.empty
 
-let preamble _ _ usf = 
-  str ";; This extracted scheme code relies on some additional macros\n" ++ 
+let preamble _ _ usf =
+  str ";; This extracted scheme code relies on some additional macros\n" ++
   str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
   str "(load \"macros_extr.scm\")\n\n" ++
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
-let pr_id id = 
+let pr_id id =
   let s = string_of_id id in
-  for i = 0 to String.length s - 1 do 
+  for i = 0 to String.length s - 1 do
     if s.[i] = '\'' then s.[i] <- '~'
-  done; 
+  done;
   str s
 
 let paren = pp_par true
 
-let pp_abst st = function 
+let pp_abst st = function
   | [] -> assert false
   | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
-  | l -> paren 
+  | l -> paren
 	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
 
-let pp_apply st _ = function 
-  | [] -> st 
+let pp_apply st _ = function
+  | [] -> st
   | [a] -> hov 2 (paren (st ++ spc () ++ a))
-  | args -> hov 2 (paren (str "@ " ++ st ++ 
+  | args -> hov 2 (paren (str "@ " ++ st ++
 			  (prlist_strict (fun x -> spc () ++ x) args)))
 
 (*s The pretty-printer for Scheme syntax *)
@@ -62,50 +62,50 @@ let pp_global k r = str (Common.pp_global k r)
 
 (*s Pretty-printing of expressions.  *)
 
-let rec pp_expr env args = 
-  let apply st = pp_apply st true args in 
+let rec pp_expr env args =
+  let apply st = pp_apply st true args in
   function
-    | MLrel n -> 
+    | MLrel n ->
 	let id = get_db_name n env in apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr env []) args' in
         pp_expr env (stl @ args) f
-    | MLlam _ as a -> 
+    | MLlam _ as a ->
       	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
 	apply (pp_abst (pp_expr env' [] a') (List.rev fl))
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id] env in
-	apply 
-	  (hv 0 
-	     (hov 2 
-		(paren 
-		   (str "let " ++ 
-		    paren 
-		      (paren 
-			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) 
+	apply
+	  (hv 0
+	     (hov 2
+		(paren
+		   (str "let " ++
+		    paren
+		      (paren
+			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1))
 		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
-    | MLglob r -> 
+    | MLglob r ->
 	apply (pp_global Term r)
     | MLcons (i,r,args') ->
 	assert (args=[]);
-	let st = 
-	  str "`" ++ 
-	  paren (pp_global Cons r ++ 
+	let st =
+	  str "`" ++
+	  paren (pp_global Cons r ++
 		 (if args' = [] then mt () else spc ()) ++
 		 prlist_with_sep spc (pp_cons_args env) args')
-	in 
-	if i = Coinductive then paren (str "delay " ++ st) else st 
+	in
+	if i = Coinductive then paren (str "delay " ++ st) else st
     | MLcase ((i,_),t, pv) ->
-	let e = 
-	  if i <> Coinductive then pp_expr env [] t 	
+	let e =
+	  if i <> Coinductive then pp_expr env [] t 
 	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
-	in 
+	in
 	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix env' i (Array.of_list (List.rev ids'),defs) args
-    | MLexn s -> 
+    | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	paren (str "error" ++ spc () ++ qs s)
     | MLdummy ->
@@ -114,36 +114,36 @@ let rec pp_expr env args =
 	pp_expr env args a
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
 
-and pp_cons_args env = function 
-  | MLcons (i,r,args) when i<>Coinductive -> 
-      paren (pp_global Cons r ++ 
+and pp_cons_args env = function
+  | MLcons (i,r,args) when i<>Coinductive ->
+      paren (pp_global Cons r ++
 	     (if args = [] then mt () else spc ()) ++
 	     prlist_with_sep spc (pp_cons_args env) args)
   | e -> str "," ++ pp_expr env [] e
-	
 
-and pp_one_pat env (r,ids,t) = 
+
+and pp_one_pat env (r,ids,t) =
   let ids,env' = push_vars (List.rev ids) env in
-  let args = 
-    if ids = [] then mt () 
+  let args =
+    if ids = [] then mt ()
     else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
-  in 
+  in
   (pp_global Cons r ++ args), (pp_expr env' [] t)
-  
-and pp_pat env pv = 
-  prvect_with_sep fnl  
-    (fun x -> let s1,s2 = pp_one_pat env x in 
+
+and pp_pat env pv =
+  prvect_with_sep fnl
+    (fun x -> let s1,s2 = pp_one_pat env x in
      hov 2 (str "((" ++ s1 ++ str ")" ++ spc () ++ s2 ++ str ")")) pv
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
 
 and pp_fix env j (ids,bl) args =
-    paren 
+    paren
       (str "letrec " ++
-       (v 0 (paren 
+       (v 0 (paren
 	       (prvect_with_sep fnl
-		  (fun (fi,ti) -> 
+		  (fun (fi,ti) ->
 		     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
 		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
 	     fnl () ++
@@ -153,50 +153,50 @@ and pp_fix env j (ids,bl) args =
 
 let pp_decl = function
   | Dind _ -> mt ()
-  | Dtype _ -> mt () 
+  | Dtype _ -> mt ()
   | Dfix (rv, defs,_) ->
-      let ppv = Array.map (pp_global Term) rv in 
-      prvect_with_sep fnl 
-	(fun (pi,ti) -> 
-	   hov 2 
-	     (paren (str "define " ++ pi ++ spc () ++ 
-		     (pp_expr (empty_env ()) [] ti)) 
+      let ppv = Array.map (pp_global Term) rv in
+      prvect_with_sep fnl
+	(fun (pi,ti) ->
+	   hov 2
+	     (paren (str "define " ++ pi ++ spc () ++
+		     (pp_expr (empty_env ()) [] ti))
 	      ++ fnl ()))
 	(array_map2 (fun p b -> (p,b)) ppv defs) ++
       fnl ()
   | Dterm (r, a, _) ->
-      if is_inline_custom r then mt () 
-      else 
-	if is_custom r then 
-	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ 
-			  str (find_custom r))) ++ fnl () ++ fnl () 
-	else 
+      if is_inline_custom r then mt ()
+      else
+	if is_custom r then
+	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
+			  str (find_custom r))) ++ fnl () ++ fnl ()
+	else
 	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
 			  pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
 
-let pp_structure_elem = function 
+let pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d
-  | (l,SEmodule m) -> 
+  | (l,SEmodule m) ->
       failwith "TODO: Scheme extraction of modules not implemented yet"
-  | (l,SEmodtype m) -> 
+  | (l,SEmodtype m) ->
       failwith "TODO: Scheme extraction of modules not implemented yet"
 
-let pp_struct = 
-  let pp_sel (mp,sel) = 
-    push_visible mp None; 
-    let p = prlist_strict pp_structure_elem sel in 
+let pp_struct =
+  let pp_sel (mp,sel) =
+    push_visible mp None;
+    let p = prlist_strict pp_structure_elem sel in
     pop_visible (); p
   in
   prlist_strict pp_sel
 
 let scheme_descr = {
-  keywords = keywords;  
-  file_suffix = ".scm"; 
-  capital_file = false;  
-  preamble = preamble; 
-  pp_struct = pp_struct; 
+  keywords = keywords;
+  file_suffix = ".scm";
+  capital_file = false;
+  preamble = preamble;
+  pp_struct = pp_struct;
   sig_suffix = None;
-  sig_preamble = (fun _ _ _ -> mt ()); 
-  pp_sig = (fun _ -> mt ()); 
-  pp_decl = pp_decl; 
+  sig_preamble = (fun _ _ _ -> mt ());
+  pp_sig = (fun _ -> mt ());
+  pp_decl = pp_decl;
 }
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 573bb9cef..b0fa395c6 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -8,4 +8,4 @@
 
 (*i $Id$ i*)
 
-val scheme_descr : Miniml.language_descr 
+val scheme_descr : Miniml.language_descr
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 66cb8d4e1..1612c8dd8 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -27,73 +27,73 @@ let occur_kn_in_ref kn = function
   | ConstructRef ((kn',_),_) -> kn = kn'
   | ConstRef _ -> false
   | VarRef _ -> assert false
-      
-let modpath_of_r = function 
+
+let modpath_of_r = function
   | ConstRef kn -> con_modpath kn
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) -> modpath kn
   | VarRef _ -> assert false
-      
-let label_of_r = function 
+
+let label_of_r = function
   | ConstRef kn -> con_label kn
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) -> label kn
   | VarRef _ -> assert false
 
-let rec base_mp = function 
-  | MPdot (mp,l) -> base_mp mp 
-  | mp -> mp 
+let rec base_mp = function
+  | MPdot (mp,l) -> base_mp mp
+  | mp -> mp
 
 let rec mp_length = function
   | MPdot (mp, _) -> 1 + (mp_length mp)
   | _ -> 1
 
-let is_modfile = function 
-  | MPfile _ -> true 
+let is_modfile = function
+  | MPfile _ -> true
   | _ -> false
 
-let string_of_modfile = function 
+let string_of_modfile = function
   | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
   | _ -> assert false
 
-let rec modfile_of_mp = function 
+let rec modfile_of_mp = function
   | (MPfile _) as mp -> mp
-  | MPdot (mp,_) -> modfile_of_mp mp 
+  | MPdot (mp,_) -> modfile_of_mp mp
   | _ -> raise Not_found
 
 let current_toplevel () = fst (Lib.current_prefix ())
 
-let is_toplevel mp = 
+let is_toplevel mp =
   mp = initial_path || mp = current_toplevel ()
 
-let at_toplevel mp = 
+let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
 let visible_kn kn = at_toplevel (base_mp (modpath kn))
 let visible_con kn = at_toplevel (base_mp (con_modpath kn))
 
-let rec prefixes_mp mp = match mp with 
+let rec prefixes_mp mp = match mp with
   | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
-  | _ -> MPset.singleton mp 
+  | _ -> MPset.singleton mp
 
 let rec get_nth_label_mp n = function
   | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
   | _ -> failwith "get_nth_label: not enough MPdot"
 
-let common_prefix_from_list mp0 mpl = 
-  let prefixes = prefixes_mp mp0 in 
-  let rec f = function 
+let common_prefix_from_list mp0 mpl =
+  let prefixes = prefixes_mp mp0 in
+  let rec f = function
     | [] -> raise Not_found
-    | mp :: l -> if MPset.mem mp prefixes then mp else f l 
+    | mp :: l -> if MPset.mem mp prefixes then mp else f l
   in f mpl
 
-let rec parse_labels ll = function 
-  | MPdot (mp,l) -> parse_labels (l::ll) mp 
+let rec parse_labels ll = function
+  | MPdot (mp,l) -> parse_labels (l::ll) mp
   | mp -> mp,ll
 
-let labels_of_mp mp = parse_labels [] mp 
+let labels_of_mp mp = parse_labels [] mp
 
-let labels_of_ref r = 
+let labels_of_ref r =
  let mp,_,l =
   match r with
      ConstRef con -> repr_con con
@@ -103,17 +103,17 @@ let labels_of_ref r =
  in
   parse_labels [l] mp
 
-let rec add_labels_mp mp = function 
-  | [] -> mp 
+let rec add_labels_mp mp = function
+  | [] -> mp
   | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
 
 
 (*S The main tables: constants, inductives, records, ... *)
 
-(* Theses tables are not registered within coq save/undo mechanism 
+(* Theses tables are not registered within coq save/undo mechanism
    since we reset their contents at each run of Extraction *)
 
-(*s Constants tables. *) 
+(*s Constants tables. *)
 
 let terms = ref (Cmap.empty : ml_decl Cmap.t)
 let init_terms () = terms := Cmap.empty
@@ -123,7 +123,7 @@ let lookup_term kn = Cmap.find kn !terms
 let types = ref (Cmap.empty : ml_schema Cmap.t)
 let init_types () = types := Cmap.empty
 let add_type kn s = types := Cmap.add kn s !types
-let lookup_type kn = Cmap.find kn !types 
+let lookup_type kn = Cmap.find kn !types
 
 (*s Inductives table. *)
 
@@ -137,18 +137,18 @@ let lookup_ind kn = KNmap.find kn !inductives
 let recursors = ref Cset.empty
 let init_recursors () = recursors := Cset.empty
 
-let add_recursors env kn = 
-  let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in 
-  let mib = Environ.lookup_mind kn env in 
-  Array.iter 
-    (fun mip -> 
-       let id = mip.mind_typename in 
+let add_recursors env kn =
+  let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in
+  let mib = Environ.lookup_mind kn env in
+  Array.iter
+    (fun mip ->
+       let id = mip.mind_typename in
        let kn_rec = make_kn (Nameops.add_suffix id "_rec")
-       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in 
+       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in
        recursors := Cset.add kn_rec (Cset.add kn_rect !recursors))
     mib.mind_packets
 
-let is_recursor = function 
+let is_recursor = function
   | ConstRef kn -> Cset.mem kn !recursors
   | _ -> false
 
@@ -178,20 +178,20 @@ let modular () = !modular_ref
 
 (*s Tables synchronization. *)
 
-let reset_tables () = 
-  init_terms (); init_types (); init_inductives (); init_recursors (); 
+let reset_tables () =
+  init_terms (); init_types (); init_inductives (); init_recursors ();
   init_projs (); init_axioms ()
 
 (*s Printing. *)
 
 (* The following functions work even on objects not in [Global.env ()].
-   WARNING: for inductive objects, an extract_inductive must have been 
+   WARNING: for inductive objects, an extract_inductive must have been
    done before. *)
 
-let safe_id_of_global = function 
+let safe_id_of_global = function
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
   | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
-  | ConstructRef ((kn,i),j) -> 
+  | ConstructRef ((kn,i),j) ->
       (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
   | _ -> assert false
 
@@ -219,21 +219,21 @@ let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
 
 let err s = errorlabstrm "Extraction" s
 
-let warning_axioms () = 
-  let info_axioms = Refset.elements !info_axioms in 
-  if info_axioms = [] then () 
+let warning_axioms () =
+  let info_axioms = Refset.elements !info_axioms in
+  if info_axioms = [] then ()
   else begin
-    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in 
-    msg_warning 
+    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
+    msg_warning
       (str ("The following "^s^" must be realized in the extracted code:")
        ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
-  let log_axioms = Refset.elements !log_axioms in 
+  let log_axioms = Refset.elements !log_axioms in
   if log_axioms = [] then ()
   else begin
-    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" 
-    in 
+    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
+    in
     msg_warning
       (str ("The following logical "^s^" encountered:") ++
        hov 1
@@ -254,51 +254,51 @@ let warning_both_mod_and_cst q mp r =
     str "First choice is assumed, for the second one please use " ++
     str "fully qualified name." ++ fnl ())
 
-let error_axiom_scheme r i = 
+let error_axiom_scheme r i =
   err (str "The type scheme axiom " ++ spc () ++
-       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
-       str " type variable(s).") 
+       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++
+       str " type variable(s).")
 
-let check_inside_module () = 
-  if Lib.is_modtype () then 
+let check_inside_module () =
+  if Lib.is_modtype () then
     err (str "You can't do that within a Module Type." ++ fnl () ++
-	 str "Close it and try again.") 
-  else if Lib.is_module () then 
+	 str "Close it and try again.")
+  else if Lib.is_module () then
     msg_warning
       (str "Extraction inside an opened module is experimental.\n" ++
        str "In case of problem, close it first.\n")
 
-let check_inside_section () = 
-  if Lib.sections_are_opened () then 
+let check_inside_section () =
+  if Lib.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
 	 str "Close it and try again.")
 
-let error_constant r = 
-  err (safe_pr_global r ++ str " is not a constant.") 
+let error_constant r =
+  err (safe_pr_global r ++ str " is not a constant.")
 
-let error_inductive r = 
+let error_inductive r =
   err (safe_pr_global r ++ spc () ++ str "is not an inductive type.")
 
-let error_nb_cons () = 
+let error_nb_cons () =
   err (str "Not the right number of constructors.")
 
-let error_module_clash s = 
-  err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ 
-       str "This is not supported yet. Please do some renaming first.") 
+let error_module_clash s =
+  err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++
+       str "This is not supported yet. Please do some renaming first.")
 
-let error_unknown_module m = 
-  err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") 
+let error_unknown_module m =
+  err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
 
-let error_scheme () = 
+let error_scheme () =
   err (str "No Scheme modular extraction available yet.")
 
-let error_not_visible r = 
+let error_not_visible r =
   err (safe_pr_global r ++ str " is not directly visible.\n" ++
        str "For example, it may be inside an applied functor." ++
        str "Use Recursive Extraction to get the whole environment.")
 
-let error_MPfile_as_mod mp b = 
-  let s1 = if b then "asked" else "required" in 
+let error_MPfile_as_mod mp b =
+  let s1 = if b then "asked" else "required" in
   let s2 = if b then "extract some objects of this module or\n" else "" in
   err (str ("Extraction of file "^(string_of_modfile mp)^
 	    ".v as a module is "^s1^".\n"^
@@ -309,19 +309,19 @@ let error_record r =
   err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
        fnl () ++ str "To help extraction, please use an explicit name.")
 
-let check_loaded_modfile mp = match base_mp mp with 
-  | MPfile dp -> if not (Library.library_is_loaded dp) then 
+let check_loaded_modfile mp = match base_mp mp with
+  | MPfile dp -> if not (Library.library_is_loaded dp) then
       err (str ("Please load library "^(string_of_dirpath dp^" first.")))
   | _ -> ()
 
-let info_file f =   
-  Flags.if_verbose message 
+let info_file f =
+  Flags.if_verbose message
     ("The file "^f^" has been created by extraction.")
 
 
 (*S The Extraction auxiliary commands *)
 
-(* The objects defined below should survive an arbitrary time, 
+(* The objects defined below should survive an arbitrary time,
    so we register them to coq save/undo mechanism. *)
 
 (*s Extraction AutoInline *)
@@ -330,11 +330,11 @@ let auto_inline_ref = ref true
 
 let auto_inline () = !auto_inline_ref
 
-let _ = declare_bool_option 
+let _ = declare_bool_option
 	  {optsync = true;
 	   optname = "Extraction AutoInline";
 	   optkey = SecondaryTable ("Extraction", "AutoInline");
-	   optread = auto_inline; 
+	   optread = auto_inline;
 	   optwrite = (:=) auto_inline_ref}
 
 (*s Extraction TypeExpand *)
@@ -343,17 +343,17 @@ let type_expand_ref = ref true
 
 let type_expand () = !type_expand_ref
 
-let _ = declare_bool_option 
+let _ = declare_bool_option
 	  {optsync = true;
 	   optname = "Extraction TypeExpand";
 	   optkey = SecondaryTable ("Extraction", "TypeExpand");
-	   optread = type_expand; 
+	   optread = type_expand;
 	   optwrite = (:=) type_expand_ref}
 
 (*s Extraction Optimize *)
 
-type opt_flag = 
-    { opt_kill_dum : bool; (* 1 *) 
+type opt_flag =
+    { opt_kill_dum : bool; (* 1 *)
       opt_fix_fun : bool;   (* 2 *)
       opt_case_iot : bool;  (* 4 *)
       opt_case_idr : bool;  (* 8 *)
@@ -367,12 +367,12 @@ type opt_flag =
 
 let kth_digit n k = (n land (1 lsl k) <> 0)
 
-let flag_of_int n = 
+let flag_of_int n =
     { opt_kill_dum = kth_digit n 0;
       opt_fix_fun = kth_digit n 1;
       opt_case_iot = kth_digit n 2;
       opt_case_idr = kth_digit n 3;
-      opt_case_idg = kth_digit n 4; 
+      opt_case_idg = kth_digit n 4;
       opt_case_cst = kth_digit n 5;
       opt_case_fun = kth_digit n 6;
       opt_case_app = kth_digit n 7;
@@ -380,7 +380,7 @@ let flag_of_int n =
       opt_lin_let = kth_digit n 9;
       opt_lin_beta = kth_digit n 10 }
 
-(* For the moment, we allow by default everything except the type-unsafe 
+(* For the moment, we allow by default everything except the type-unsafe
    optimization [opt_case_idg]. *)
 
 let int_flag_init = 1 + 2 + 4 + 8 + 32 + 64 + 128 + 256 + 512 + 1024
@@ -392,19 +392,19 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
 
 let optims () = !opt_flag_ref
 
-let _ = declare_bool_option 
-	  {optsync = true; 
+let _ = declare_bool_option
+	  {optsync = true;
 	   optname = "Extraction Optimize";
 	   optkey = SecondaryTable ("Extraction", "Optimize");
-	   optread = (fun () -> !int_flag_ref <> 0); 
+	   optread = (fun () -> !int_flag_ref <> 0);
 	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
 
 let _ = declare_int_option
           { optsync = true;
             optname = "Extraction Flag";
-            optkey = SecondaryTable("Extraction","Flag"); 
-            optread = (fun _ -> Some !int_flag_ref); 
-            optwrite = (function 
+            optkey = SecondaryTable("Extraction","Flag");
+            optread = (fun _ -> Some !int_flag_ref);
+            optwrite = (function
                           | None -> chg_flag 0
                           | Some i -> chg_flag (max i 0))}
 
@@ -417,20 +417,20 @@ let lang_ref = ref Ocaml
 
 let lang () = !lang_ref
 
-let (extr_lang,_) = 
-  declare_object 
-    {(default_object "Extraction Lang") with  
+let (extr_lang,_) =
+  declare_object
+    {(default_object "Extraction Lang") with
        cache_function = (fun (_,l) -> lang_ref := l);
        load_function = (fun _ (_,l) -> lang_ref := l);
        export_function = (fun x -> Some x)}
 
-let _ = declare_summary "Extraction Lang" 
+let _ = declare_summary "Extraction Lang"
 	  { freeze_function = (fun () -> !lang_ref);
 	    unfreeze_function = ((:=) lang_ref);
 	    init_function = (fun () -> lang_ref := Ocaml);
 	    survive_module = true;
-	    survive_section = true }  
-	  
+	    survive_section = true }
+
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 (*s Extraction Inline/NoInline *)
@@ -443,22 +443,22 @@ let to_inline r = Refset.mem r (fst !inline_table)
 
 let to_keep r = Refset.mem r (snd !inline_table)
 
-let add_inline_entries b l = 
-  let f b = if b then Refset.add else Refset.remove in 
-  let i,k = !inline_table in 
-  inline_table := 
-  (List.fold_right (f b) l i), 
+let add_inline_entries b l =
+  let f b = if b then Refset.add else Refset.remove in
+  let i,k = !inline_table in
+  inline_table :=
+  (List.fold_right (f b) l i),
   (List.fold_right (f (not b)) l k)
 
 (* Registration of operations for rollback. *)
 
 let (inline_extraction,_) =
-  declare_object 
-    {(default_object "Extraction Inline") with 
+  declare_object
+    {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
-       export_function = (fun x -> Some x); 
-       classify_function = (fun (_,o) -> Substitute o); 
+       export_function = (fun x -> Some x);
+       classify_function = (fun (_,o) -> Substitute o);
        subst_function =
         (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
@@ -473,36 +473,36 @@ let _ = declare_summary "Extraction Inline"
 (* Grammar entries. *)
 
 let extraction_inline b l =
-  check_inside_section (); 
-  let refs = List.map Nametab.global l in 
-  List.iter 
-    (fun r -> match r with 
+  check_inside_section ();
+  let refs = List.map Nametab.global l in
+  List.iter
+    (fun r -> match r with
        | ConstRef _ -> ()
-       | _ -> error_constant r) refs; 
+       | _ -> error_constant r) refs;
   Lib.add_anonymous_leaf (inline_extraction (b,refs))
 
 (* Printing part *)
 
-let print_extraction_inline () = 
-  let (i,n)= !inline_table in 
-  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in 
-  msg 
-    (str "Extraction Inline:" ++ fnl () ++ 
+let print_extraction_inline () =
+  let (i,n)= !inline_table in
+  let i'= Refset.filter (function ConstRef _ -> true | _ -> false) i in
+  msg
+    (str "Extraction Inline:" ++ fnl () ++
      Refset.fold
-       (fun r p -> 
+       (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
-     str "Extraction NoInline:" ++ fnl () ++ 
+     str "Extraction NoInline:" ++ fnl () ++
      Refset.fold
-       (fun r p -> 
+       (fun r p ->
 	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
 
 (* Reset part *)
 
-let (reset_inline,_) = 
+let (reset_inline,_) =
   declare_object
-    {(default_object "Reset Extraction Inline") with  
+    {(default_object "Reset Extraction Inline") with
        cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
-       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table); 
+       load_function = (fun _ (_,_)-> inline_table :=  empty_inline_table);
        export_function = (fun x -> Some x)}
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
@@ -511,8 +511,8 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 (*s Extract Constant/Inductive. *)
 
 (* UGLY HACK: to be defined in [extraction.ml] *)
-let use_type_scheme_nb_args, register_type_scheme_nb_args = 
-  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r 
+let use_type_scheme_nb_args, register_type_scheme_nb_args =
+  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
 
 let customs = ref Refmap.empty
 
@@ -520,7 +520,7 @@ let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
 
 let is_custom r = Refmap.mem r !customs
 
-let is_inline_custom r = (is_custom r) && (to_inline r) 
+let is_inline_custom r = (is_custom r) && (to_inline r)
 
 let find_custom r = snd (Refmap.find r !customs)
 
@@ -528,13 +528,13 @@ let find_type_custom r = Refmap.find r !customs
 
 (* Registration of operations for rollback. *)
 
-let (in_customs,_) = 
-  declare_object 
-    {(default_object "ML extractions") with 
+let (in_customs,_) =
+  declare_object
+    {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
        load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
-       export_function = (fun x -> Some x); 
-       classify_function = (fun (_,o) -> Substitute o); 
+       export_function = (fun x -> Some x);
+       classify_function = (fun (_,o) -> Substitute o);
        subst_function =
         (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
@@ -550,17 +550,17 @@ let _ = declare_summary "ML extractions"
 
 let extract_constant_inline inline r ids s =
   check_inside_section ();
-  let g = Nametab.global r in 
-  match g with 
-    | ConstRef kn -> 
-	let env = Global.env () in 
-	let typ = Typeops.type_of_constant env kn in 
+  let g = Nametab.global r in
+  match g with
+    | ConstRef kn ->
+	let env = Global.env () in
+	let typ = Typeops.type_of_constant env kn in
 	let typ = Reduction.whd_betadeltaiota env typ in
-	if Reduction.is_arity env typ 
-	  then begin 
-	    let nargs = use_type_scheme_nb_args env typ in 
+	if Reduction.is_arity env typ
+	  then begin
+	    let nargs = use_type_scheme_nb_args env typ in
 	    if List.length ids <> nargs then error_axiom_scheme g nargs
-	  end; 
+	  end;
 	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,ids,s))
     | _ -> error_constant g
@@ -568,19 +568,19 @@ let extract_constant_inline inline r ids s =
 
 let extract_inductive r (s,l) =
   check_inside_section ();
-  let g = Nametab.global r in 
+  let g = Nametab.global r in
   match g with
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
 	let n = Array.length mib.mind_packets.(i).mind_consnames in
-	if n <> List.length l then error_nb_cons (); 
+	if n <> List.length l then error_nb_cons ();
 	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,[],s));
 	list_iter_i
-	  (fun j s -> 
-	     let g = ConstructRef (ip,succ j) in 
+	  (fun j s ->
+	     let g = ConstructRef (ip,succ j) in
 	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	     Lib.add_anonymous_leaf (in_customs (g,[],s))) l
-    | _ -> error_inductive g 
+    | _ -> error_inductive g
 
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index dd6e85a9d..fc29e871c 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -24,12 +24,12 @@ val error_axiom_scheme : global_reference -> int -> 'a
 val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
-val error_module_clash : string -> 'a 
+val error_module_clash : string -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
 val error_MPfile_as_mod : module_path -> bool -> 'a
-val error_record : global_reference -> 'a 
+val error_record : global_reference -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit
@@ -44,9 +44,9 @@ val label_of_r : global_reference -> label
 val current_toplevel : unit -> module_path
 val base_mp : module_path -> module_path
 val is_modfile : module_path -> bool
-val string_of_modfile : module_path -> string 
+val string_of_modfile : module_path -> string
 val is_toplevel : module_path -> bool
-val at_toplevel : module_path -> bool 
+val at_toplevel : module_path -> bool
 val visible_kn : kernel_name -> bool
 val visible_con : constant -> bool
 val mp_length : module_path -> int
@@ -69,10 +69,10 @@ val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit
 val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind
 
 val add_recursors : Environ.env -> kernel_name -> unit
-val is_recursor : global_reference -> bool 
+val is_recursor : global_reference -> bool
 
 val add_projection : int -> constant -> unit
-val is_projection : global_reference -> bool 
+val is_projection : global_reference -> bool
 val projection_arity : global_reference -> int
 
 val add_info_axiom : global_reference -> unit
@@ -81,18 +81,18 @@ val add_log_axiom : global_reference -> unit
 
 val reset_tables : unit -> unit
 
-(*s AutoInline parameter *) 
+(*s AutoInline parameter *)
 
 val auto_inline : unit -> bool
 
-(*s TypeExpand parameter *) 
+(*s TypeExpand parameter *)
 
 val type_expand : unit -> bool
 
-(*s Optimize parameter *) 
+(*s Optimize parameter *)
 
-type opt_flag = 
-    { opt_kill_dum : bool; (* 1 *) 
+type opt_flag =
+    { opt_kill_dum : bool; (* 1 *)
       opt_fix_fun : bool;   (* 2 *)
       opt_case_iot : bool;  (* 4 *)
       opt_case_idr : bool;  (* 8 *)
@@ -109,14 +109,14 @@ val optims :  unit -> opt_flag
 (*s Target language. *)
 
 type lang = Ocaml | Haskell | Scheme
-val lang : unit -> lang 
+val lang : unit -> lang
 
 (*s Extraction mode: modular or monolithic *)
 
 val set_modular : bool -> unit
-val modular : unit -> bool 
+val modular : unit -> bool
 
-(*s Table for custom inlining *) 
+(*s Table for custom inlining *)
 
 val to_inline : global_reference -> bool
 val to_keep : global_reference -> bool
@@ -137,7 +137,7 @@ val extraction_language : lang -> unit
 val extraction_inline : bool -> reference list -> unit
 val print_extraction_inline : unit -> unit
 val reset_extraction_inline : unit -> unit
-val extract_constant_inline : 
+val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
 val extract_inductive : reference -> string * string list -> unit