Modules et Records: gros changements pour prendre en compte le nouveau mind_record

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

11 files changed, 150 insertions, 143 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 150fb8fae..73648e71e 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -374,7 +374,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;
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 26a263942..f3fb85db2 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -343,40 +343,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
-	(* avoid constant projections (records fields defined with [:=]) *)
-	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 
-		(* avoid dummy arguments for projectors *)
-                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
@@ -616,7 +629,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 
@@ -689,7 +702,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. *)
 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index c55e89a51..12f7fbb1a 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -125,16 +125,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)))
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 784fc627c..84eeaa7c3 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -46,7 +46,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 +83,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 dbfd18d6b..4fa62a009 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -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,9 +741,9 @@ 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) 
+      simpl_case o i 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)) -> 
@@ -770,7 +770,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 +778,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 +801,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 +1006,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 +1061,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 +1071,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 ee3008e13..f4b84361a 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -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,10 @@ 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,_) -> record_iter_references do_term i; do_cons r 
+      | MLcase (i,_,v) as a -> 
+	  record_iter_references do_term i; 
+	  Array.iter (fun (r,_,_) -> do_cons r) v
       | _ -> ()
   in iter a
 
@@ -180,7 +186,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); 
+  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 = 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index f4daa5a7a..1e5473234 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -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
@@ -167,6 +165,10 @@ 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. *)
 
@@ -193,7 +195,7 @@ let rec pp_type par vl t =
 
 let expr_needs_par = function
   | MLlam _  -> true
-  | MLcase (_,[|_|]) -> false 
+  | MLcase (_,_,[|_|]) -> false 
   | MLcase _ -> true
   | _        -> false 
 
@@ -231,30 +233,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 +267,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 +289,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 +311,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 +335,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 "  " ++
@@ -420,8 +421,7 @@ 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 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 " = { "++
@@ -466,13 +466,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; 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index babe170c2..1cc686cdf 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -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 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 84daae82b..1149a7f69 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -77,7 +77,7 @@ 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 "`" ++ 
@@ -87,17 +87,13 @@ let rec pp_expr env args =
 		   (fun () -> spc () ++ str ",") 
 		   (pp_expr 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-case " ++ 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
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 54b083e18..d6358e956 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -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 ecc6588b3..4c88f68b5 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -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