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

1 files changed, 9 insertions, 3 deletions

diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index ee3008e135..f4b84361ab 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 =