Imported Upstream version 8.0pl3upstream/8.0pl3

18 files changed, 387 insertions, 271 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 53a2631e..8e441613 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.ml,v 1.51.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: common.ml,v 1.51.2.4 2005/12/16 03:07:39 letouzey Exp $ i*)
 
 open Pp
 open Util
@@ -269,11 +269,18 @@ module StdParams = struct
 
   (* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *)
 
+  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
+
   let rec dottify = function 
     | [] -> assert false 
-    | [s] -> s 
-    | s::[""] -> s 
-    | s::l -> (dottify l)^"."^s
+    | [s] -> unquote s 
+    | s::[""] -> unquote s 
+    | s::l -> (dottify l)^"."^(unquote s)
 
   let pp_global mpl r = 
     let ls = get_renamings r in 
@@ -353,7 +360,7 @@ let preamble prm = match lang () with
   | Ocaml -> Ocaml.preamble prm   
   | Haskell -> Haskell.preamble prm
   | Scheme -> Scheme.preamble prm
-  | Toplevel -> (fun _ _ -> mt ())
+  | Toplevel -> (fun _ _ _ -> mt ())
 
 let preamble_sig prm = match lang () with 
   | Ocaml -> Ocaml.preamble_sig prm   
@@ -374,7 +381,6 @@ let info f =
     (str ("The file "^f^" has been created by extraction."))
 
 let print_structure_to_file f prm struc =
-  cons_cofix := Refset.empty;
   Hashtbl.clear renamings;
   mod_1st_level := Idmap.empty; 
   modcontents := Gset.empty;
@@ -387,9 +393,13 @@ let print_structure_to_file f prm struc =
     else (create_mono_renamings struc; [])
   in 
   let print_dummys =
-    (struct_ast_search MLdummy struc, 
+    (struct_ast_search ((=) MLdummy) struc, 
      struct_type_search Tdummy struc, 
      struct_type_search Tunknown struc)
+  in 
+  let print_magic = 
+    if lang () <> Haskell then false 
+    else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
   in
   (* print the implementation *)
   let cout = option_app (fun (f,_) -> open_out f) f in 
@@ -397,7 +407,7 @@ let print_structure_to_file f prm struc =
     | None -> !Pp_control.std_ft
     | Some cout -> Pp_control.with_output_to cout in 
   begin try 
-    msg_with ft (preamble prm used_modules print_dummys);
+    msg_with ft (preamble prm used_modules print_dummys print_magic);
     msg_with ft (pp_struct struc);
     option_iter close_out cout; 
   with e -> 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 46bf06dd..6bfe861f 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml,v 1.136.2.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: extraction.ml,v 1.136.2.4 2005/12/01 11:27:15 letouzey Exp $ i*)
 
 (*i*)
 open Util
@@ -183,15 +183,17 @@ let rec extract_type env db j c args =
 	   | (Info, Default) -> 
 	       (* Standard case: two [extract_type] ... *)
 	       let mld = extract_type env' (0::db) j d [] in 
-	       if mld = Tdummy then Tdummy 
+	       if type_eq (mlt_env env) mld Tdummy then Tdummy 
 	       else Tarr (extract_type env db 0 t [], mld) 
 	   | (Info, TypeScheme) when j > 0 -> 
 	       (* A new type var. *)
 	       let mld = extract_type env' (j::db) (j+1) d [] in 
-	       if mld = Tdummy then Tdummy else Tarr (Tdummy, mld)
+	       if type_eq (mlt_env env) mld Tdummy then Tdummy 
+	       else Tarr (Tdummy, mld)
 	   | _ -> 
 	       let mld = extract_type env' (0::db) j d [] in 
-	       if mld = Tdummy then Tdummy else Tarr (Tdummy, mld))
+	       if type_eq (mlt_env env) mld Tdummy then Tdummy 
+	       else Tarr (Tdummy, mld))
     | Sort _ -> Tdummy (* The two logical cases. *)
     | _ when sort_of env (applist (c, args)) = InProp -> Tdummy 
     | Rel n -> 
@@ -343,38 +345,53 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	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 
-	if is_custom (IndRef ip) then raise (I Standard); 
-	let projs = 
-	  try (find_structure ip).s_PROJ 
-	  with Not_found -> raise (I Standard);
+	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 
+	  | Prod(n,_,t) -> n::(names_prod t)
+	  | LetIn(_,_,_,t) -> names_prod t
+	  | Cast(t,_) -> names_prod t
+	  | _ -> []
 	in 
-	let n = nb_default_params env mip0.mind_nf_arity in
-	let projs = try List.map out_some projs with _ -> raise (I Standard) in
-	let is_true_proj kn = 
-          let (_,body) = Sign.decompose_lam_assum (constant_value env kn) in
-          match kind_of_term body with
-              | Rel _ -> false
-              | Case _ -> true
-              | _ -> assert false
+	let field_names = 
+	  list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in 
+	assert (List.length field_names = List.length typ);
+	let projs = ref KNset.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 type_eq (mlt_env env) Tdummy typ then select_fields l typs 
+	      else  
+		let knp = make_kn mp d (label_of_id id) in 
+		if not (List.mem false (type_to_sign (mlt_env env) typ)) then 
+		  projs := KNset.add knp !projs; 
+		(ConstRef knp) :: (select_fields l typs)
+	  | Anonymous::l, typ::typs -> 
+	      if type_eq (mlt_env env) Tdummy typ then select_fields l typs
+	      else error_record r
+	  | _ -> assert false 
 	in 
-	let projs = List.filter is_true_proj projs in 
- 	let rec check = function 
-          | [] -> [],[]
-          | (typ, kn) :: l -> 
-              let l1,l2 = check l in 
-              if type_eq (mlt_env env) Tdummy typ then l1,l2 
-              else 
-                let r = ConstRef kn in 
-                if List.mem false (type_to_sign (mlt_env env) typ) 
-                then r :: l1, l2 
-                else r :: l1, r :: l2
-	in 
-	add_record kn n (check (List.combine typ projs)); 
-	raise (I Record)
+	let field_glob = select_fields field_names typ
+	in
+	(* Is this record officially declared with its projections ? *)
+	(* If so, we use this information. *)
+	begin try 
+	  let n = nb_default_params env mip0.mind_nf_arity in
+	  List.iter 
+	    (option_iter 
+	       (fun kn -> if KNset.mem kn !projs then add_projection n kn))
+	    (find_structure ip).s_PROJ 
+	with Not_found -> ()
+	end; 
+	Record field_glob
       with (I info) -> info
     in
-    let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in 
+    let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in
     add_ind kn i; 
     internal_call := KNset.remove kn !internal_call;
     i
@@ -564,7 +581,9 @@ and extract_cst_app env mle mlt kn args =
   (* Different situations depending of the number of arguments: *)
   if ls = 0 then put_magic_if magic2 head
   else if List.mem true s then 
-    if la >= ls then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
+    if la >= ls || not (List.mem false s) 
+    then 
+      put_magic_if (magic2 && not magic1) (MLapp (head, mla))
     else 
       (* Not enough arguments. We complete via eta-expansion. *)
       let ls' = ls-la in
@@ -599,7 +618,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvars, type_cons) in 
   (* Then, the usual variables [s], [ls], [la], ... *)
-  let s = List.map ((<>) Tdummy) types in
+  let s = List.map (type_neq env Tdummy) types in
   let ls = List.length s in 
   let la = List.length args in 
   assert (la <= ls + params_nb);
@@ -614,7 +633,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   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 (ConstructRef cp, mla))
+    else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
   in 
   (* Different situations depending of the number of arguments: *)
   if la < params_nb then 
@@ -670,10 +689,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	(* The types of the arguments of the corresponding constructor. *)
 	let f t = type_subst_vect metas (type_expand env t) in 
 	let l = List.map f oi.ip_types.(i) in
+	(* the corresponding signature *)
+	let s = List.map (type_neq env Tdummy) 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 
 	(* We suppress dummy arguments according to signature. *)
-	let ids,e = case_expunge (List.map ((<>) Tdummy) l) e in
+	let ids,e = case_expunge s e in
 	(ConstructRef (ip,i+1), List.rev ids, e)
       in
       if mi.ind_info = Singleton then 
@@ -687,7 +708,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	end 
       else 
 	(* Standard case: we apply [extract_branch]. *)
-	MLcase (a, Array.init br_size extract_branch)
+	MLcase (mi.ind_info, a, Array.init br_size extract_branch)
   
 (*s Extraction of a (co)-fixpoint. *)
 
@@ -726,7 +747,7 @@ let extract_std_constant env kn body typ =
   (* The real type [t']: without head lambdas, expanded, *)
   (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
   let l,t' = type_decomp (type_expand env (var2var' t)) in 
-  let s = List.map ((<>) Tdummy) l in 
+  let s = List.map (type_neq env Tdummy) l in 
   (* The initial ML environment. *)
   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
   (* Decomposing the top level lambdas of [body]. *)
@@ -836,7 +857,8 @@ let logical_decl = function
   | Dterm (_,MLdummy,Tdummy) -> true
   | Dtype (_,[],Tdummy) -> true 
   | Dfix (_,av,tv) -> 
-      (array_for_all ((=) MLdummy) av) && (array_for_all ((=) Tdummy) tv)
+      (array_for_all ((=) MLdummy) av) && 
+      (array_for_all ((=) Tdummy) tv)
   | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 29c8cd18..3834fe81 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.ml,v 1.40.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: haskell.ml,v 1.40.2.5 2005/12/16 04:11:28 letouzey Exp $ i*)
 
 (*s Production of Haskell syntax. *)
 
@@ -27,23 +27,41 @@ let keywords =
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
-    "as"; "qualified"; "hiding" ; "unit" ]
+    "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
   Idset.empty
 
-let preamble prm used_modules (mldummy,tdummy,tunknown) =
+let preamble prm used_modules (mldummy,tdummy,tunknown) magic =
   let pp_mp = function 
     | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
     | _ -> assert false 
   in  
+  (if not 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 prm.mod_name ++ str " where" ++ fnl () 
   ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
   prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
   ++ fnl () ++
-  (if mldummy then 
+  (if not magic then mt () 
+   else str "\
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+import qualified IOExts
+unsafeCoerce = IOExts.unsafeCoerce
+#endif")
+  ++
+  fnl() ++ fnl() 
+  ++
+  (if not mldummy then mt () 
+   else
      str "__ = Prelude.error \"Logical or arity value used\"" 
-     ++ fnl () ++ fnl()
-   else mt())
+     ++ fnl () ++ fnl())
 
 let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO" 
 
@@ -61,27 +79,36 @@ module Make = functor(P : Mlpp_param) -> struct
 
 let local_mpl = ref ([] : module_path list)
 
-let pp_global r = P.pp_global !local_mpl r
+let pp_global r = 
+  if is_inline_custom r then str (find_custom r) 
+  else P.pp_global !local_mpl r
+
 let empty_env () = [], P.globals()
 
 (*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 
+  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 
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global r	
     | Tglob (r,l) -> 
-	pp_par par 
-	  (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
+	if r = IndRef (kn_sig,0) then 
+	  pp_type true vl (List.hd l)
+	else 
+	  pp_par par 
+	    (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy -> str "()"
     | Tunknown -> str "()"
     | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
-    | Tcustom s -> str s
  in 
   hov 0 (pp_rec par t)
 
@@ -125,16 +152,16 @@ let rec pp_expr par env args =
 		 spc () ++ hov 0 pp_a2)))
     | MLglob r -> 
 	apply (pp_global r)
-    | MLcons (r,[]) ->
+    | MLcons (_,r,[]) ->
 	assert (args=[]); pp_global r
-    | MLcons (r,[a]) ->
+    | MLcons (_,r,[a]) ->
 	assert (args=[]);
 	pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a)
-    | MLcons (r,args') ->
+    | MLcons (_,r,args') ->
 	assert (args=[]);
 	pp_par par (pp_global r ++ spc () ++ 
 		    prlist_with_sep spc (pp_expr true env []) args')
-    | MLcase (t, pv) ->
+    | MLcase (_,t, pv) ->
       	apply (pp_par par' 
 		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
 		       fnl () ++ str "  " ++ pp_pat env pv)))
@@ -146,7 +173,8 @@ let rec pp_expr par env args =
 	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
-    | MLmagic a ->  pp_expr par env args 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 pv = 
@@ -210,7 +238,7 @@ let pp_one_ind ip pl cv =
        | [] -> (mt ()) 
        | _  -> (str " " ++
       	       	prlist_with_sep 
-		  (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
+		  (fun () -> (str " ")) (pp_type true pl) l))
   in
   str (if cv = [||] then "type " else "data ") ++ 
   pp_global (IndRef ip) ++ str " " ++
@@ -239,6 +267,8 @@ let rec pp_ind first kn i ind =
 
 (*s Pretty-printing of a declaration. *)
 
+let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
+
 let pp_decl mpl = 
   local_mpl := mpl;
   function
@@ -248,21 +278,32 @@ let pp_decl mpl =
   | Dtype (r, l, t) ->
       if is_inline_custom r then mt () 
       else 
-	let l = rename_tvars keywords l in
-	let l' = List.rev l in 
-	hov 2 (str "type " ++ pp_global r ++ spc () ++ 
-	       prlist (fun id -> pr_id id ++ str " ") l ++
-	       str "=" ++ spc () ++ pp_type false l' t) ++ fnl () ++ fnl ()
+	let l = rename_tvars keywords l in 
+	let st = 
+	  try 
+	    let ids,s = find_type_custom r in 
+	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
+	  with not_found -> 
+	    prlist (fun id -> pr_id id ++ str " ") l ++
+	    if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
+	    else str "=" ++ spc () ++ pp_type false l t
+	in 
+	hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl ()
   | Dfix (rv, defs,_) ->
       let ppv = Array.map pp_global rv in 
       prlist_with_sep (fun () -> fnl () ++ fnl ())
 	(fun (pi,ti) -> pp_function (empty_env ()) pi ti)
 	(List.combine (Array.to_list ppv) (Array.to_list defs)) 
       ++ fnl () ++ fnl ()
-  | Dterm (r, a, _) ->
+  | Dterm (r, a, t) ->
       if is_inline_custom r then mt () 
       else 
-	hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ())
+	let e = pp_global r in 
+	e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
+	  if is_custom r then 	
+	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl() ++ fnl ())
+	  else 
+	    hov 0 (pp_function (empty_env ()) e a ++ fnl () ++ fnl ())
 
 let pp_structure_elem mpl = function 
   | (l,SEdecl d) -> pp_decl mpl d
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 4da5db0c..822444bd 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.mli,v 1.15.6.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: haskell.mli,v 1.15.6.2 2005/12/01 17:01:22 letouzey Exp $ i*)
 
 open Pp
 open Names
@@ -15,6 +15,6 @@ open Miniml
 val keywords : Idset.t
 
 val preamble : 
-  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 866ff847..7c18f9f5 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: miniml.mli,v 1.46.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*)
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
@@ -35,7 +35,6 @@ type ml_type =
   | Tdummy
   | Tunknown
   | Taxiom
-  | Tcustom of string
 
 and ml_meta = { id : int; mutable contents : ml_type option }
 
@@ -46,7 +45,11 @@ type ml_schema = int * ml_type
 
 (*s ML inductive types. *)
 
-type inductive_info = Record | Singleton | Coinductive | Standard
+type inductive_info = 
+  | Singleton 
+  | Coinductive 
+  | Standard 
+  | Record of global_reference list 
 
 (* 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
@@ -79,8 +82,9 @@ type ml_ast =
   | MLlam    of identifier * ml_ast
   | MLletin  of identifier * ml_ast * ml_ast
   | MLglob   of global_reference
-  | MLcons   of global_reference * ml_ast list
-  | MLcase   of ml_ast * (global_reference * identifier list * ml_ast) array
+  | MLcons   of inductive_info * global_reference * ml_ast list
+  | MLcase   of inductive_info * ml_ast * 
+      (global_reference * identifier list * ml_ast) array
   | MLfix    of int * identifier array * ml_ast array
   | MLexn    of string
   | MLdummy
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index fbe423a7..c01766b0 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.ml,v 1.104.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: mlutil.ml,v 1.104.2.3 2005/12/01 16:28:04 letouzey Exp $ i*)
 
 (*i*)
 open Pp
@@ -117,9 +117,9 @@ let rec mgu = function
 
 let needs_magic p = try mgu p; false with Impossible -> true
 
-let put_magic_if b a = if b then MLmagic a else a
+let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
 
-let put_magic p a = if needs_magic p then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
 
 
 (*S ML type env. *)
@@ -327,11 +327,11 @@ let ast_iter_rel f =
     | MLrel i -> f (i-n)
     | MLlam (_,a) -> iter (n+1) a
     | MLletin (_,a,b) -> iter n a; iter (n+1) b
-    | MLcase (a,v) ->
+    | MLcase (_,a,v) ->
 	iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v
     | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
-    | MLcons (_,l) ->  List.iter (iter n) l
+    | MLcons (_,_,l) ->  List.iter (iter n) l
     | MLmagic a -> iter n a
     | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
   in iter 0 
@@ -343,10 +343,10 @@ let ast_map_case f (c,ids,a) = (c,ids,f a)
 let ast_map f = function
   | MLlam (i,a) -> MLlam (i, f a)
   | MLletin (i,a,b) -> MLletin (i, f a, f b)
-  | MLcase (a,v) -> MLcase (f a, Array.map (ast_map_case f) v)
+  | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v)
   | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
   | MLapp (a,l) -> MLapp (f a, List.map f l)
-  | MLcons (c,l) -> MLcons (c, List.map f l)
+  | MLcons (i,c,l) -> MLcons (i,c, List.map f l)
   | MLmagic a -> MLmagic (f a)
   | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
 
@@ -357,11 +357,11 @@ 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 
   | MLlam (i,a) -> MLlam (i, f (n+1) a)
   | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
-  | MLcase (a,v) -> MLcase (f n a,Array.map (ast_map_lift_case f n) v)
+  | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) 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 (c,l) -> MLcons (c, 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	
 
@@ -372,10 +372,10 @@ let ast_iter_case f (c,ids,a) = f a
 let ast_iter f = function
   | MLlam (i,a) -> f a
   | MLletin (i,a,b) -> f a; f b
-  | MLcase (a,v) -> f a; Array.iter (ast_iter_case f) v
+  | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v
   | MLfix (i,ids,v) -> Array.iter f v
   | MLapp (a,l) -> f a; List.iter f l
-  | MLcons (c,l) -> List.iter f l
+  | MLcons (_,c,l) -> List.iter f l
   | MLmagic a -> f a
   | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> ()
 
@@ -411,7 +411,7 @@ let nb_occur t = nb_occur_k 1 t
 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 
 	  (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
@@ -420,7 +420,7 @@ let nb_occur_match =
       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
@@ -616,7 +616,7 @@ let check_and_generalize (r0,l,c) =
 	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) -> 
+    | 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  
@@ -707,7 +707,7 @@ let rec permut_case_fun br acc =
 
 let rec is_iota_gen = function 
   | MLcons _ -> true
-  | MLcase(_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
+  | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
   | _ -> false
 
 let constructor_index = function
@@ -716,15 +716,15 @@ let constructor_index = function
 
 let iota_gen br = 
   let rec iota k = function 
-    | MLcons (r,a) ->
+    | 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 
 	MLapp (c,a)
-    | MLcase(e,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(e, new_br)
+	in MLcase(i,e, new_br)
     | _ -> assert false
   in iota 0 
 
@@ -741,13 +741,18 @@ let rec simpl o = function
       simpl o f
   | MLapp (f, a) -> 
       simpl_app o (List.map (simpl o) a) (simpl o f)
-  | MLcase (e,br) ->
+  | MLcase (i,e,br) ->
       let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in 
-      simpl_case o br (simpl o e) 
-  | MLletin(id,c,e) when 
-      (id = dummy_name) || (is_atomic c) || (is_atomic e) ||
-      (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let)) -> 
+      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 
 	simpl o (ast_subst c e)
+      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 
@@ -770,7 +775,7 @@ and simpl_app o a = function
   | 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 (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 
@@ -778,16 +783,16 @@ and simpl_app o a = function
 	     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 (e,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 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 
-    try (* Does a term [f] exist such as each branch is [(f e)] ? *)
+    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 
       simpl o (MLapp (MLlam (anonymous,f),[e]))
@@ -801,9 +806,9 @@ and simpl_case o br e =
 	then 
 	  let ids,br = permut_case_fun br [] in 
 	  let n = List.length ids in 
-	  if n <> 0 then named_lams ids (MLcase (ast_lift n e, br))
-	  else MLcase (e, br) 
-	else MLcase (e,br)
+	  if n <> 0 then named_lams ids (MLcase (i,ast_lift n e, br))
+	  else MLcase (i,e,br) 
+	else MLcase (i,e,br)
 
 let rec post_simpl = function 
   | MLletin(_,c,e) when (is_atomic (eta_red c)) -> 
@@ -1006,8 +1011,8 @@ let optimize_fix a =
 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) -> 
+  | MLcons(_,_,l) -> ml_size_list l
+  | 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
@@ -1061,7 +1066,7 @@ let rec non_stricts add cand = function
   | MLapp (t,l)-> 
       let cand = non_stricts false cand t in 
       List.fold_left (non_stricts false) cand l 
-  | MLcons (_,l) -> 
+  | MLcons (_,_,l) -> 
       List.fold_left (non_stricts false) cand l
   | MLletin (_,t1,t2) -> 
       let cand = non_stricts false cand t1 in 
@@ -1071,7 +1076,7 @@ let rec non_stricts add cand = function
       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). *)
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index feb9e54e..54f0c992 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.ml,v 1.7.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: modutil.ml,v 1.7.2.4 2005/12/01 17:01:22 letouzey Exp $ i*)
 
 open Names
 open Declarations
@@ -157,6 +157,10 @@ let struct_iter do_decl do_spec s =
 
 type do_ref = global_reference -> unit
 
+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 
@@ -169,8 +173,12 @@ let ast_iter_references do_term do_cons do_type a =
     ast_iter iter a;
     match a with 
       | MLglob r -> do_term r
-      | MLcons (r,_) -> do_cons r
-      | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> do_cons r) v
+      | MLcons (i,r,_) -> 
+	  if lang () = Ocaml then record_iter_references do_term i; 
+	  do_cons r 
+      | MLcase (i,_,v) as a -> 
+	  if lang () = Ocaml then record_iter_references do_term i; 
+	  Array.iter (fun (r,_,_) -> do_cons r) v
       | _ -> ()
   in iter a
 
@@ -180,7 +188,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
   let packet_iter ip p = 
     do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
   in
-  if ind.ind_info = Record then List.iter do_term (find_projections kn); 
+  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 = 
@@ -236,7 +244,7 @@ let struct_get_references_list struc =
 exception Found
 
 let rec ast_search t a = 
-  if t = a then raise Found else ast_iter (ast_search t) a
+  if t a then raise Found else ast_iter (ast_search t) a
 
 let decl_ast_search t = function 
   | Dterm (_,a,_) -> ast_search t a
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index f73e18f7..7f8c4113 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.mli,v 1.2.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: modutil.mli,v 1.2.2.2 2005/12/01 17:01:22 letouzey Exp $ i*)
 
 open Names
 open Declarations
@@ -42,7 +42,7 @@ val add_labels_mp : module_path -> label list -> module_path
 
 (*s Functions upon ML modules. *)
 
-val struct_ast_search : ml_ast -> ml_structure -> bool
+val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
 val struct_type_search : ml_type -> ml_structure -> bool
 
 type do_ref = global_reference -> unit 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 707ef94f..ff9cfd21 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.ml,v 1.100.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: ocaml.ml,v 1.100.2.6 2005/12/01 17:01:22 letouzey Exp $ i*)
 
 (*s Production of Ocaml syntax. *)
 
@@ -20,8 +20,6 @@ open Miniml
 open Mlutil
 open Modutil
 
-let cons_cofix = ref Refset.empty
-
 (*s Some utility functions. *)
 
 let pp_par par st = if par then str "(" ++ st ++ str ")" else st
@@ -68,6 +66,12 @@ let sec_space_if = function true -> spc () | false -> mt ()
 
 let fnl2 () = fnl () ++ fnl () 
 
+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<>[])) 
+
 (*s Generic renaming issues. *)
 
 let rec rename_id id avoid = 
@@ -126,7 +130,7 @@ let keywords =
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] 
   Idset.empty
 
-let preamble _ used_modules (mldummy,tdummy,tunknown) = 
+let preamble _ used_modules (mldummy,tdummy,tunknown) _ = 
   let pp_mp = function 
     | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
     | _ -> assert false 
@@ -167,22 +171,33 @@ let pp_global r =
 
 let empty_env () = [], P.globals ()
 
+exception NoRecord
+
+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 
+  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)) 
 		 with _ -> (str "'a" ++ int i))
     | Tglob (r,[]) -> pp_global r
-    | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global r
+    | Tglob (r,l) -> 
+	if r = IndRef (kn_sig,0) then 
+	  pp_tuple_light pp_rec l
+	else 
+	  pp_tuple_light pp_rec l ++ spc () ++ pp_global r
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
     | Tdummy -> str "__"
     | Tunknown -> str "__"
-    | Tcustom s -> str s
   in 
   hov 0 (pp_rec par t)
 
@@ -193,7 +208,7 @@ let rec pp_type par vl t =
 
 let expr_needs_par = function
   | MLlam _  -> true
-  | MLcase (_,[|_|]) -> false 
+  | MLcase (_,_,[|_|]) -> false 
   | MLcase _ -> true
   | _        -> false 
 
@@ -231,30 +246,32 @@ let rec pp_expr par env args =
 	   let record = List.hd args in 
 	   pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
 	 with _ -> apply (pp_global r))
-    | MLcons (r,[]) ->
+    | MLcons (Coinductive,r,[]) ->
 	assert (args=[]);
-	if Refset.mem r !cons_cofix then 
-	  pp_par par (str "lazy " ++ pp_global r)
-	else pp_global r
-    | MLcons (r,args') -> 
-	(try 
-	   let projs = find_projections (kn_of_r r) in 
-	   pp_record_pat (projs, List.map (pp_expr true env []) args')
-	 with Not_found ->
-	   assert (args=[]);
-	   let tuple = pp_tuple (pp_expr true env []) args' in 
-	   if Refset.mem r !cons_cofix then 
-	     pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
-	   else pp_par par (pp_global r ++ spc () ++ tuple))
-    | MLcase (t, pv) ->
+	pp_par par (str "lazy " ++ pp_global r)
+    | MLcons (Coinductive,r,args') -> 
+	assert (args=[]);
+	let tuple = pp_tuple (pp_expr true env []) args' in 
+	pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
+    | MLcons (_,r,[]) -> 
+	assert (args=[]);
+	pp_global r
+    | MLcons (Record projs, r, args') -> 
+	assert (args=[]); 
+	pp_record_pat (projs, List.map (pp_expr true env []) args')
+    | MLcons (_,r,args') -> 
+	assert (args=[]);
+	let tuple = pp_tuple (pp_expr true env []) args' in 
+	pp_par par (pp_global r ++ spc () ++ tuple)
+    | MLcase (i, t, pv) ->
 	let r,_,_ = pv.(0) in 
-	let expr = if Refset.mem r !cons_cofix 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 (kn_of_r r) in 
+	   let projs = find_projections i in 
 	   let (_, ids, c) = pv.(0) in 
 	   let n = List.length ids in 
 	   match c with 
@@ -263,17 +280,17 @@ let rec pp_expr par env args =
 				     pp_global (List.nth projs (n-i)))) 
 	     | MLapp (MLrel i, a) when i <= n -> 
 		 if List.exists (ast_occurs_itvl 1 n) a 
-		 then raise Not_found
+		 then raise NoRecord
 		 else
 		   let ids,env' = push_vars (List.rev ids) env in
 		   (pp_apply 
 		      (pp_expr true env [] t ++ str "." ++ 
 		       pp_global (List.nth projs (n-i)))
 		      par ((List.map (pp_expr true env' []) a) @ args))
-	     | _ -> raise Not_found
-	 with Not_found -> 
+	     | _ -> raise NoRecord
+	 with NoRecord -> 
 	   if Array.length pv = 1 then 
-	     let s1,s2 = pp_one_pat env pv.(0) in 
+	     let s1,s2 = pp_one_pat env i pv.(0) in 
 	     apply 
 	       (hv 0 
 		  (pp_par par' 
@@ -285,7 +302,7 @@ let rec pp_expr par env args =
 	     apply
       	       (pp_par par' 
       		  (v 0 (str "match " ++ expr ++ str " with" ++
-			fnl () ++ str "  | " ++ pp_pat env pv))))
+			fnl () ++ str "  | " ++ pp_pat env i 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
@@ -307,21 +324,21 @@ and pp_record_pat (projs, args) =
      (List.combine projs args) ++
    str " }"
 
-and pp_one_pat env (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 (kn_of_r r) in 
+    let projs = find_projections i in 
     pp_record_pat (projs, List.rev_map pr_id ids), expr
-  with Not_found -> 
+  with NoRecord -> 
     let args = 
       if ids = [] then (mt ()) 
       else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in 
     pp_global r ++ args, expr
   
-and pp_pat env pv = 
+and pp_pat env i pv = 
   prvect_with_sep (fun () -> (fnl () ++ str "  | ")) 
-    (fun x -> let s1,s2 = pp_one_pat env x in 
+    (fun x -> let s1,s2 = pp_one_pat env i x in 
      hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv
 
 and pp_function env f t =
@@ -331,20 +348,17 @@ and pp_function env f t =
     let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
     not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl)
   in
-  let is_not_cofix pv = 
-    let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix) 
-  in					  
   match t' with 
-    | MLcase(MLrel 1,pv) when is_not_cofix pv ->
+    | MLcase(i,MLrel 1,pv) when i=Standard ->
 	if is_function pv then
 	  (f ++ pr_binding (List.rev (List.tl bl)) ++
        	     str " = function" ++ fnl () ++
-	     v 0 (str "  | " ++ pp_pat env' pv))
+	     v 0 (str "  | " ++ pp_pat env' i pv))
 	else
           (f ++ pr_binding (List.rev bl) ++ 
              str " = match " ++
 	     pr_id (List.hd bl) ++ str " with" ++ fnl () ++
-	     v 0 (str "  | " ++ pp_pat env' pv))
+	     v 0 (str "  | " ++ pp_pat env' i pv))
 	  
     | _ -> (f ++ pr_binding (List.rev bl) ++
 	      str " =" ++ fnl () ++ str "  " ++
@@ -384,12 +398,6 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
 	
 (*s Pretty-printing of inductive types declaration. *)
 
-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_one_ind prefix ip pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
@@ -420,9 +428,8 @@ let pp_singleton kn packet =
 	 pp_comment (str "singleton inductive, whose constructor was " ++ 
 		     pr_id packet.ip_consnames.(0)))
 
-let pp_record kn packet = 
-  let l = List.combine (find_projections kn) packet.ip_types.(0) in 
-  let projs = find_projections kn in
+let pp_record kn projs packet = 
+  let l = List.combine projs packet.ip_types.(0) in 
   let pl = rename_tvars keywords packet.ip_vars in 
   str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
   hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
@@ -466,13 +473,9 @@ let pp_ind co kn ind =
 let pp_mind kn i = 
   match i.ind_info with 
     | Singleton -> pp_singleton kn i.ind_packets.(0)
-    | Coinductive -> 
-	let nop _ = () 
-	and add r = cons_cofix := Refset.add r !cons_cofix in 
-	decl_iter_references nop add nop (Dind (kn,i)); 
-	pp_ind true kn i
-    | Record -> pp_record kn i.ind_packets.(0)
-    | _ -> pp_ind false kn i
+    | Coinductive -> pp_ind true kn i
+    | Record projs -> pp_record kn projs i.ind_packets.(0)
+    | Standard -> pp_ind false kn i
 
 let pp_decl mpl = 
   local_mpl := mpl; 
@@ -481,6 +484,7 @@ let pp_decl mpl =
     | Dtype (r, l, t) ->
 	if is_inline_custom r then failwith "empty phrase"
 	else 
+	  let pp_r = pp_global r in 
 	  let l = rename_tvars keywords l in 
 	  let ids, def = try 
 	    let ids,s = find_type_custom r in 
@@ -490,7 +494,7 @@ let pp_decl mpl =
 	    if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
 	    else str "=" ++ spc () ++ pp_type false l t
 	  in 
-	  hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ 
+	  hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++ 
 		 spc () ++ def)
     | Dterm (r, a, t) -> 
 	if is_inline_custom r then failwith "empty phrase"
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 711c15da..5015a50d 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.mli,v 1.26.6.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: ocaml.mli,v 1.26.6.3 2005/12/01 17:01:22 letouzey Exp $ i*)
 
 (*s Some utility functions to be reused in module [Haskell]. *)
 
@@ -15,8 +15,6 @@ open Names
 open Libnames
 open Miniml
 
-val cons_cofix : Refset.t ref
-
 val pp_par : bool -> std_ppcmds -> std_ppcmds
 val pp_abst : identifier list -> std_ppcmds
 val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds 
@@ -39,10 +37,10 @@ val get_db_name : int -> env -> identifier
 val keywords : Idset.t
 
 val preamble : 
-  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
 
 val preamble_sig : 
-  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+  extraction_params -> module_path list -> bool*bool*bool -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 61045304..4a881da2 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.ml,v 1.9.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: scheme.ml,v 1.9.2.5 2005/12/16 03:07:39 letouzey Exp $ i*)
 
 (*s Production of Scheme syntax. *)
 
@@ -24,17 +24,30 @@ open Ocaml
 
 let keywords =     
   List.fold_right (fun s -> Idset.add (id_of_string s))
-    [ "define"; "let"; "lambda"; "lambdas"; "match-case"; 
+    [ "define"; "let"; "lambda"; "lambdas"; "match"; 
       "apply"; "car"; "cdr"; 
       "error"; "delay"; "force"; "_"; "__"] 
     Idset.empty
 
-let preamble _ _ (mldummy,_,_) = 
+let preamble _ _ (mldummy,_,_) _ = 
+  str ";; This extracted scheme code relies on some additional macros" ++ 
+  fnl () ++
+  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++
+  fnl () ++
+  str "(load \"macros_extr.scm\")" ++
+  fnl () ++ fnl () ++
   (if mldummy then 
      str "(define __ (lambda (_) __))" 
      ++ fnl () ++ fnl()
    else mt ())
 
+let pr_id id = 
+  let s = string_of_id id in
+  for i = 0 to String.length s - 1 do 
+    if s.[i] = '\'' then s.[i] <- '~'
+  done; 
+  str s
+
 let paren = pp_par true
 
 let pp_abst st = function 
@@ -43,6 +56,12 @@ let pp_abst st = function
   | l -> paren 
 	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
 
+let pp_apply st _ = function 
+  | [] -> st 
+  | [a] -> hov 2 (paren (st ++ spc () ++ a))
+  | args -> hov 2 (paren (str "@ " ++ st ++ 
+			  (prlist (fun x -> spc () ++ x) args))) 
+
 (*s The pretty-printing functor. *)
 
 module Make = functor(P : Mlpp_param) -> struct
@@ -63,7 +82,7 @@ let rec pp_expr env args =
     | MLlam _ as a -> 
       	let fl,a' = collect_lams a in
 	let fl,env' = push_vars fl env in
-	pp_abst (pp_expr env' [] a') (List.rev fl)
+	apply (pp_abst (pp_expr env' [] a') (List.rev fl))
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id] env in
 	apply 
@@ -77,46 +96,46 @@ let rec pp_expr env args =
 		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r -> 
 	apply (pp_global r)
-    | MLcons (r,args') ->
+    | MLcons (i,r,args') ->
 	assert (args=[]);
 	let st = 
 	  str "`" ++ 
 	  paren (pp_global r ++ 
-		 (if args' = [] then mt () else (spc () ++ str ",")) ++
-		 prlist_with_sep 
-		   (fun () -> spc () ++ str ",") 
-		   (pp_expr env []) args')
+		 (if args' = [] then mt () else spc ()) ++
+		 prlist_with_sep spc (pp_cons_args env) args')
 	in 
-	if Refset.mem r !cons_cofix then 
-	  paren (str "delay " ++ st)
-        else st 
-    | MLcase (t, pv) ->
-	let r,_,_ = pv.(0) in 
-	let e = if Refset.mem r !cons_cofix then 
-	  paren (str "force" ++ spc () ++ pp_expr env [] t)
-	else 
-	  pp_expr env [] t 	
-	in apply (v 3 (paren 
-			 (str "match-case " ++ e ++ fnl () ++ pp_pat env pv)))
+	if i = Coinductive then paren (str "delay " ++ st) else st 
+    | MLcase (i,t, pv) ->
+	let e = 
+	  if i <> Coinductive then pp_expr env [] t 	
+	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
+	in 
+	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s -> 
 	(* An [MLexn] may be applied, but I don't really care. *)
-	paren (str "absurd")
+	paren (str "error" ++ spc () ++ qs s)
     | MLdummy ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLmagic a ->
 	pp_expr env args a
-    | MLaxiom -> paren (str "absurd ;;AXIOM TO BE REALIZED\n")
+    | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
+
+and pp_cons_args env = function 
+  | MLcons (i,r,args) when i<>Coinductive -> 
+      paren (pp_global 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) = 
-  let pp_arg id = str "?" ++ pr_id id in 
   let ids,env' = push_vars (List.rev ids) env in
   let args = 
     if ids = [] then mt () 
-    else (str " " ++ prlist_with_sep spc pp_arg (List.rev ids))
+    else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
   in 
   (pp_global r ++ args), (pp_expr env' [] t)
   
@@ -133,7 +152,8 @@ and pp_fix env j (ids,bl) args =
       (str "letrec " ++
        (v 0 (paren 
 	       (prvect_with_sep fnl
-		  (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti)))
+		  (fun (fi,ti) -> 
+		     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
 		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
 	     fnl () ++
       	     hov 2 (pp_apply (pr_id (ids.(j))) true args))))
@@ -156,8 +176,12 @@ let pp_decl _ = function
   | Dterm (r, a, _) ->
       if is_inline_custom r then mt () 
       else 
-	hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
-		      pp_expr (empty_env ()) [] a)) ++ fnl ()  ++ fnl ()
+	if is_custom r then 
+	  hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ 
+			  str (find_custom r))) ++ fnl () ++ fnl () 
+	else 
+	  hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+			  pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
 
 let pp_structure_elem mp = function 
   | (l,SEdecl d) -> pp_decl mp d
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 6e689a47..2a828fb9 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.mli,v 1.6.6.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: scheme.mli,v 1.6.6.2 2005/12/01 17:01:22 letouzey Exp $ i*)
 
 (*s Some utility functions to be reused in module [Haskell]. *)
 
@@ -17,7 +17,7 @@ open Names
 val keywords : Idset.t
 
 val preamble : 
-  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index a65c51a4..9d73d13f 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml,v 1.35.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: table.ml,v 1.35.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
 
 open Names
 open Term
@@ -90,17 +90,9 @@ let is_recursor = function
 
 (*s Record tables. *)
 
-let records = ref (KNmap.empty : global_reference list KNmap.t)
-let init_records () = records := KNmap.empty
-
 let projs = ref (Refmap.empty : int Refmap.t)
 let init_projs () = projs := Refmap.empty
-
-let add_record kn n (l1,l2) = 
-  records := KNmap.add kn l1 !records; 
-  projs := List.fold_right (fun r -> Refmap.add r n) l2 !projs
-
-let find_projections kn = KNmap.find kn !records
+let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
 let is_projection r = Refmap.mem r !projs
 let projection_arity r = Refmap.find r !projs
 
@@ -108,7 +100,7 @@ let projection_arity r = Refmap.find r !projs
 
 let reset_tables () = 
   init_terms (); init_types (); init_inductives (); init_recursors (); 
-  init_records (); init_projs ()
+  init_projs ()
 
 (*s Printing. *)
 
@@ -196,6 +188,10 @@ let error_MPfile_as_mod d =
   err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
 	    "Extraction cannot currently deal with this situation.\n"))
 
+let error_record r = 
+  err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++
+       str "To help extraction, please use an explicit name.") 
+
 (*S The Extraction auxiliary commands *)
 
 (*s Extraction AutoInline *)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 680638e5..6160452a 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.mli,v 1.25.2.1 2004/07/16 19:30:09 herbelin Exp $ i*)
+(*i $Id: table.mli,v 1.25.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
 
 open Names
 open Libnames
@@ -29,7 +29,7 @@ val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
 val error_unqualified_name : string -> string -> 'a 
 val error_MPfile_as_mod : dir_path -> 'a
-
+val error_record : global_reference -> 'a 
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 
@@ -58,9 +58,7 @@ val lookup_ind : kernel_name -> ml_ind
 val add_recursors : Environ.env -> kernel_name -> unit
 val is_recursor : global_reference -> bool 
 
-val add_record : 
-  kernel_name -> int -> global_reference list * global_reference list -> unit
-val find_projections : kernel_name -> global_reference list
+val add_projection : int -> kernel_name -> unit
 val is_projection : global_reference -> bool 
 val projection_arity : global_reference -> int
 
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index b358ff39..1500e1ae 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -157,11 +157,9 @@ let rec npatternify ltypes c =
   | [] -> c
   | (mv,nme,t)::ltypes' -> 
      let c'= substitterm 0 mv (mkRel 1) c in
-(*      let _ = prconstr c' in *)
      let tlift = lift (List.length ltypes') t in
      let res = 
       npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in
-(*      let _ = prconstr res in *)
      res
 
 (* fait une application (c m1 m2...mn, où mi est une evar, on rend également
@@ -510,15 +508,15 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs:
   | u -> 
      let varrels = List.rev (List.map fst lst_vars) in
      let varnames = List.map snd lst_vars in
-     let nb_vars = (List.length varnames) in
-     let nb_eqs = (List.length lst_eqs) in
+     let nb_vars = List.length varnames in
+     let nb_eqs = List.length lst_eqs in
      let eqrels = List.map fst lst_eqs in
      (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs
         trouvés dans les let in et les Cases avec ceux trouves dans u (ie
         mi.mimick). *)
      (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *)
-     let terms_recs = lst_recs @ (hdMatchSub_cpl mi.mimick mi.fonc)  in
-     
+     let terms_recs = lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in
+
      (*c construction du terme: application successive des variables, des
        egalites et des appels rec, a la variable existentielle correspondant a
        l'hypothese de recurrence en cours. *)
@@ -573,7 +571,6 @@ let invfun_proof fonc def_fonc gl_abstr pis env sigma =
  sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in
  let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in
  princ_proof,levar,lposeq,evararr,absc,parms
-
 (* Do intros [i] times, then do rewrite on all introduced hyps which are called
    like [heq_prefix], FIX: have another filter than the name. *)
 let rec iterintro i = 
@@ -596,12 +593,12 @@ let rec iterintro i =
 
 (* 
        (fun hyp gl -> 
-        let _ = print_string ("nthhyp= "^ string_of_int i) in
+        let _ = prstr ("nthhyp= "^ string_of_int i) in
         if isConst hyp && ((name_of_const hyp)==heq_prefix) then
-          let _ = print_string "YES\n" in
+          let _ = prstr "YES\n" in
           rewriteLR hyp gl 
         else 
-          let _ = print_string "NO\n" in
+          let _ = prstr "NO\n" in
           tclIDTAC gl)
  *)
     
@@ -818,9 +815,9 @@ let buildFunscheme fonc mutflist =
     
 (* Declaration of the functional scheme. *)
 let declareFunScheme f fname mutflist =
- let scheme = 
-   buildFunscheme (constr_of f) 
-    (Array.of_list (List.map constr_of (f::mutflist))) in
+ let flist = if mutflist=[] then [f] else mutflist in
+ let fcstrlist = Array.of_list (List.map constr_of flist) in
+ let scheme = buildFunscheme (constr_of f) fcstrlist in
   let _ = prstr "Principe:" in
   let _ = prconstr scheme in
  let ce = { 
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 6e086d95..a125b9a7 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -21,7 +21,7 @@ open Reductionops
 (*s printing of constr -- debugging *)
 
 (* comment this line to see debug msgs *)
-let msg x = () ;; let prterm c = str "" 
+let msg x = () ;; let prterm c = str ""
   (* uncomment this to see debugging *)
 let prconstr c =  msg (str"  " ++ prterm c ++ str"\n")
 let prlistconstr lc = List.iter prconstr lc
@@ -194,52 +194,53 @@ let rec buildrefl_from_eqs eqs =
 
 
 
-(* list of occurrences of a term inside another, no imbricated
-   occurrence are considered (ie we stop looking inside a termthat is
-   an occurrence). *)
+(* list of occurrences of a term inside another *)
+(* Cofix will be wrong, not sure Fix is correct too *)
 let rec hdMatchSub u t=
-  if constr_head_match u t then 
-	 u::(fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
-      [] 
-      u)
-  else
-    fold_constr (fun l cstr -> l@(hdMatchSub cstr t))
-      [] 
-      u
+  let subres = 
+    match kind_of_term u with
+      | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t
+      | Fix (_,(lna,tl,bl))  -> 
+	  Array.fold_left 
+	    (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) 
+	    [] bl
+      | LetIn _  -> assert false
+	  (* Correct? *)
+      | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u
+  in 
+  if constr_head_match u t then u :: subres else subres
+
 
 (* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *)
 let hdMatchSub_cpl u (d,f) = 
-	 let res = ref [] in
-	 begin
-	 	for i = d to f do res := (hdMatchSub u (mkRel i)) @ !res done;
-		  !res
-	 end
+  let res = ref [] in
+  begin
+    for i = d to f do res := hdMatchSub u (mkRel i) @ !res done;
+    !res
+  end
 
 
 (* destApplication raises an exception if [t] is not an application *)      
 let exchange_hd_prod subst_hd t =
-    let (hd,args)= destApplication t in mkApp (subst_hd,args)
+  let hd,args= destApplication t in mkApp (subst_hd,args)
 
 (* substitute t by by_t in head of products inside in_u, reduces each
 	product found  *)
 let rec substit_red prof t by_t in_u =
   if constr_head_match in_u (lift prof t) 
   then
-	 let _ = prNamedConstr "in_u" in_u in
-	 let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
-	 let _ = prNamedConstr "xx " x in
-	 let _ = prstr "\n\n" in
-	 x
+    let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in
+    x
   else
-    map_constr_with_binders succ (fun i u -> substit_red i t by_t u)
-    	prof in_u
+    map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u
 
 (* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
 	reli by tarr.(f-i). *) 
 let exchange_reli_arrayi tarr (d,f) t =
   let hd,args= destApplication t in 
   let i = destRel hd in
-  whd_beta (mkApp (tarr.(f-i) ,args))
+  let res = whd_beta (mkApp (tarr.(f-i) ,args)) in
+  res
 
 let exchange_reli_arrayi_L tarr (d,f) = 
   List.map (exchange_reli_arrayi tarr (d,f))
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 50f5b947..02dc57de 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -195,6 +195,11 @@ let xlate_int_opt = function
   | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n)
   | None ->  CT_coerce_NONE_to_INT_OPT CT_none
 
+let xlate_int_or_var_opt_to_int_opt = function
+  | Some (ArgArg n) -> CT_coerce_INT_to_INT_OPT (CT_int n)
+  | Some (ArgVar _) -> xlate_error "int_or_var: TODO"
+  | None ->  CT_coerce_NONE_to_INT_OPT CT_none
+
 let tac_qualid_to_ct_ID ref = 
   CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref)))
 
@@ -1026,12 +1031,12 @@ and xlate_tac =
         (if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none),
         (if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none))
     | TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
-    | TacAuto (nopt, Some []) -> CT_auto (xlate_int_opt nopt)
+    | TacAuto (nopt, Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
     | TacAuto (nopt, None) ->
- 	CT_auto_with (xlate_int_opt nopt,
+ 	CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt,
 		      CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
     | TacAuto (nopt, Some (id1::idl)) ->
-	CT_auto_with(xlate_int_opt nopt,
+	CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt,
              CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
              CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
     |TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) ->
@@ -1141,7 +1146,8 @@ and xlate_tac =
     | TacClearBody([]) -> assert false
     | TacClearBody(a::l) -> 
 	CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
-    | TacDAuto (a, b) -> CT_dauto(xlate_int_opt a, xlate_int_opt b)
+    | TacDAuto (a, b) ->
+	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
     | TacNewDestruct(a,b,(c,_)) ->
 	CT_new_destruct
 	  (xlate_int_or_constr a, xlate_using b, 
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index f2eeb5fe..f0eb1e78 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -13,7 +13,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* $Id: omega.ml,v 1.7.2.1 2004/07/16 19:30:13 herbelin Exp $ *) 
+(* $Id: omega.ml,v 1.7.2.2 2005/02/17 18:25:20 herbelin Exp $ *) 
 
 open Util
 open Hashtbl
@@ -520,9 +520,11 @@ let rec depend relie_on accu = function
 	      depend (e1.id::e2.id::relie_on) (act::accu) l
             else 
 	      depend relie_on accu l
-	| STATE (e,_,_,_,_) ->
-            if List.mem e.id relie_on then depend relie_on (act::accu) l
-            else depend relie_on accu l
+	| STATE (e,_,o,_,_) ->
+            if List.mem e.id relie_on then
+	      depend (o.id::relie_on) (act::accu) l
+            else
+	      depend relie_on accu l
 	| HYP e ->   
             if List.mem e.id relie_on then depend relie_on (act::accu) l
             else depend relie_on accu l