bug concernant les projecteurs de Record avec args logiques

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

3 files changed, 19 insertions, 10 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 824a48568f..1636e12db0 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -345,13 +345,21 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  try (find_structure ip).s_PROJ 
 	  with Not_found -> raise (I Standard);
 	in 
-	let s = List.map (type_neq (mlt_env env) Tdummy) typ in
 	let n = nb_default_params env mip0.mind_nf_arity in
-	let check (_,o) = match o with 
-	  | None -> raise (I Standard)
-	  | Some kn -> ConstRef kn 
-	in  
-	add_record kn n (List.map check (List.filter fst (List.combine s projs))); 
+	let rec check = function 
+          | [] -> [],[]
+          | (typ, kno) :: l -> 
+              let l1,l2 = check l in 
+              if type_eq (mlt_env env) Tdummy typ then l1,l2 
+              else match kno with 
+                | None -> raise (I Standard) 
+                | Some kn -> 
+                    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)
       with (I info) -> info
     in
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 7afc2f9ea7..a7ed138632 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -100,9 +100,9 @@ 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 l = 
-  records := KNmap.add kn l !records; 
-  projs := List.fold_right (fun r -> Refmap.add r n) l !projs
+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 is_projection r = Refmap.mem r !projs
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 087d7f8468..32aecd6135 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -56,7 +56,8 @@ 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 -> unit
+val add_record : 
+  kernel_name -> int -> global_reference list * global_reference list -> unit
 val find_projections : kernel_name -> global_reference list
 val is_projection : global_reference -> bool 
 val projection_arity : global_reference -> int