Extraction: allow extraction of records with anonymous fields (fix #2555)

 For Ocaml, we now use the extraction-reserved substring "__" :
 The name foo__i will be pick for i-th field of record foo if it is anonymous.

 For Haskell, still no printing of records as native records,
 hence nothing to do.

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

1 files changed, 11 insertions, 14 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 54fdbcaeaa..b9c42c30d5 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -443,17 +443,16 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let mp,d,_ = repr_mind kn in
 	let rec select_fields l typs = match l,typs with
 	  | [],[] -> []
-	  | (Name id)::l, typ::typs ->
-	      if isDummy (expand env typ) then select_fields l typs
-	      else
-		let knp = make_con mp d (label_of_id id) in
-		if List.for_all ((=) Keep) (type2signature env typ)
-		then
-		  projs := Cset.add knp !projs;
-		(ConstRef knp) :: (select_fields l typs)
+	  | _::l, typ::typs when isDummy (expand env typ) ->
+	      select_fields l typs
 	  | Anonymous::l, typ::typs ->
-	      if isDummy (expand env typ) then select_fields l typs
-	      else error_record r
+	      None :: (select_fields l typs)
+	  | Name id::l, typ::typs ->
+	      let knp = make_con mp d (label_of_id id) in
+	      (* Is it safe to use [id] for projections [foo.id] ? *)
+	      if List.for_all ((=) Keep) (type2signature env typ)
+	      then projs := Cset.add knp !projs;
+	      Some (ConstRef knp) :: (select_fields l typs)
 	  | _ -> assert false
 	in
 	let field_glob = select_fields field_names typ
@@ -464,10 +463,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  let n = nb_default_params env
             (Inductive.type_of_inductive env (mib,mip0))
 	  in
-	  List.iter
-	    (Option.iter
-	       (fun kn -> if Cset.mem kn !projs then add_projection n kn))
-	    (lookup_projections ip)
+	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn in
+	  List.iter (Option.iter check_proj) (lookup_projections ip)
 	with Not_found -> ()
 	end;
 	Record field_glob