From 4a602e4d159c68eaa127e636df0d3445bfe998a2 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 25 Jun 2004 00:00:12 +0000
Subject: correspondance des records et noms de champs de records entre un
 module et sa signature

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/extraction.ml | 2 ++
 contrib/extraction/ocaml.ml      | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 247bd137b5..26a263942a 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -351,6 +351,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	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
@@ -366,6 +367,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
               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
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 0498987b32..f4daa5a7aa 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -421,8 +421,8 @@ let pp_singleton kn packet =
 		     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 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 ()) 
-- 
cgit v1.2.3