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

1 files changed, 385 insertions, 385 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f9e2799a19..a4d2445ecd 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