Imported Upstream version 8.3.pl3upstream/8.3.pl3

29 files changed, 221 insertions, 139 deletions

diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index 882bcae9..eab2f67c 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index 69e72918..e38d41e3 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index 697ea6b3..b059b2a0 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 61dc7313..1fb83c5b 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index da0af5cc..e577ebe1 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index f8f942c8..48260e3d 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index 54b314de..5ca6bd7b 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index b302cd36..a7046626 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index 4c33691d..ae04ba6d 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9cea0562..9713fcd2 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
+(*i $Id: common.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Pp
 open Util
@@ -179,6 +179,16 @@ let mktable autoclean =
   if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
   (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
 
+(* We might have built [global_reference] whose canonical part is
+   inaccurate. We must hence compare only the user part,
+   hence using a Hashtbl might be incorrect *)
+
+let mktable_ref autoclean =
+  let m = ref Refmap'.empty in
+  let clear () = m := Refmap'.empty in
+  if autoclean then register_cleanup clear;
+  (fun r v -> m := Refmap'.add r v !m), (fun r -> Refmap'.find r !m), clear
+
 (* A table recording objects in the first level of all MPfile *)
 
 let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
@@ -355,10 +365,10 @@ let ref_renaming_fun (k,r) =
 (* Cached version of the last function *)
 
 let ref_renaming =
-  let add,get,_ = mktable true in
-  fun x ->
-    try if is_mp_bound (base_mp (modpath_of_r (snd x))) then raise Not_found; get x
-    with Not_found -> let y = ref_renaming_fun x in add x y; y
+  let add,get,_ = mktable_ref true in
+  fun ((k,r) as x) ->
+    try if is_mp_bound (base_mp (modpath_of_r r)) then raise Not_found; get r
+    with Not_found -> let y = ref_renaming_fun x in add r y; y
 
 (* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
    can be printed as [s] in the current context of visible
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index f6ff76ba..22bad6cd 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.mli 14010 2011-04-15 16:05:07Z letouzey $ i*)
+(*i $Id: common.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Libnames
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7d4cd770..3fa674d3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 14012 2011-04-15 16:45:27Z letouzey $ i*)
+(*i $Id: extract_env.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Term
 open Declarations
@@ -404,10 +404,18 @@ let print_one_decl struc mp decl =
 
 (*s Extraction of a ml struct to a file. *)
 
+(** For Recursive Extraction, writing directly on stdout
+    won't work with coqide, we use a buffer instead *)
+
+let buf = Buffer.create 1000
+
 let formatter dry file =
   let ft =
     if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
-    else Pp_control.with_output_to (Option.default stdout file)
+    else
+      match file with
+	| Some f -> Pp_control.with_output_to f
+	| None -> Format.formatter_of_buffer buf
   in
   (* We never want to see ellipsis ... in extracted code *)
   Format.pp_set_max_boxes ft max_int;
@@ -421,6 +429,7 @@ let formatter dry file =
   ft
 
 let print_structure_to_file (fn,si,mo) dry struc =
+  Buffer.clear buf;
   let d = descr () in
   reset_renaming_tables AllButExternal;
   let unsafe_needs = {
@@ -463,7 +472,12 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 close_out cout; raise e
        end;
        info_file si)
-    (if dry then None else si)
+    (if dry then None else si);
+  (* Print the buffer content via Coq standard formatter (ok with coqide). *)
+  if Buffer.length buf <> 0 then begin
+    Pp.message (Buffer.contents buf);
+    Buffer.reset buf
+  end
 
 
 (*********************************************)
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index b4516898..145cd6b3 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extract_env.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*s This module declares the extraction commands. *)
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b9a3a736..27f32a4a 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 13795 2011-01-22 14:43:06Z glondu $ i*)
+(*i $Id: extraction.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
 
 (*i*)
 open Util
@@ -36,9 +36,17 @@ let current_fixpoints = ref ([] : constant list)
 
 let none = Evd.empty
 
-let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
+let type_of env c =
+  try
+    let polyprop = (lang() = Haskell) in
+    Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
+  with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
-let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
+let sort_of env c =
+  try
+    let polyprop = (lang() = Haskell) in
+    Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
+  with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
 let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None
 
@@ -423,17 +431,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
@@ -444,10 +451,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
@@ -561,7 +566,11 @@ let rec extract_term env mle mlt c args =
 	  let a = new_meta () in
 	  let c1' = extract_term env mle a c1 [] in
 	  (* The type of [c1'] is generalized and stored in [mle]. *)
-	  let mle' = Mlenv.push_gen mle a in
+	  let mle' =
+	    if generalizable c1'
+	    then Mlenv.push_gen mle a
+	    else Mlenv.push_type mle a
+	  in
 	  MLletin (Id id, c1', extract_term env' mle' mlt c2 args')
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 0574b009..8a2125fe 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extraction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*s Extraction from Coq terms to Miniml. *)
 
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index fb25e7d1..ebd4de0d 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 17a38136..aeacef93 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
+(*i $Id: haskell.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*s Production of Haskell syntax. *)
 
@@ -47,6 +47,7 @@ let preamble mod_name used_modules usf =
   (if used_modules = [] then mt () else fnl ()) ++
   (if not usf.magic then mt ()
    else str "\
+unsafeCoerce :: a -> b
 #ifdef __GLASGOW_HASKELL__
 import qualified GHC.Base
 unsafeCoerce = GHC.Base.unsafeCoerce#
@@ -57,7 +58,8 @@ unsafeCoerce = IOExts.unsafeCoerce
 #endif" ++ fnl2 ())
   ++
   (if not usf.mldummy then mt ()
-   else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
+   else str "__ :: any" ++ fnl () ++
+        str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
 
 let pp_abst = function
   | [] -> (mt ())
diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli
index 0b68e73b..eb774db7 100644
--- a/plugins/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: haskell.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 val haskell_descr : Miniml.language_descr
 
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 20092815..aaf2d0c3 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: miniml.mli 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: miniml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
@@ -57,7 +57,7 @@ type inductive_kind =
   | Singleton
   | Coinductive
   | Standard
-  | Record of global_reference list
+  | Record of global_reference option list (* None for anonymous field *)
 
 (* 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
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index c242e4ab..3c7ee0f2 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.ml 14003 2011-04-14 23:09:41Z letouzey $ i*)
+(*i $Id: mlutil.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -119,6 +119,7 @@ let rec mgu = function
       mgu (a, a'); mgu (b, b')
   | Tglob (r,l), Tglob (r',l') when r = r' ->
        List.iter mgu (List.combine l l')
+  | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> ()
   | Tdummy _, Tdummy _ -> ()
   | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
   | _ -> raise Impossible
@@ -129,6 +130,11 @@ let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
 
 let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
 
+let generalizable a =
+  lang () <> Ocaml ||
+    match a with
+      | MLapp _ -> false
+      | _ -> true (* TODO, this is just an approximation for the moment *)
 
 (*S ML type env. *)
 
@@ -961,10 +967,18 @@ let kill_some_lams bl (ids,c) =
 let kill_dummy_lams c =
   let ids,c = collect_lams c in
   let bl = List.map sign_of_id ids in
-  if (List.mem Keep bl) && (List.exists isKill bl) then
-    let ids',c = kill_some_lams bl (ids,c) in
-    ids, named_lams ids' c
-  else raise Impossible
+  if not (List.mem Keep bl) then raise Impossible;
+  let rec fst_kill n = function
+    | [] -> raise Impossible
+    | Kill _ :: bl -> n
+    | Keep :: bl -> fst_kill (n+1) bl
+  in
+  let skip = max 0 ((fst_kill 0 bl) - 1) in
+  let ids_skip, ids = list_chop skip ids in
+  let _, bl = list_chop skip bl in
+  let c = named_lams ids_skip c in
+  let ids',c = kill_some_lams bl (ids,c) in
+  ids, named_lams ids' c
 
 (*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c]
    and a signature [s] and builds a eta-long version. *)
@@ -1005,21 +1019,26 @@ let term_expunge s (ids,c) =
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
-(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and
-  purge the args of [t0] corresponding to a [dummy_name].
+(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+  purge the args of [MLrel r] corresponding to a [dummy_name].
   It makes eta-expansion if needed. *)
 
-let kill_dummy_args ids t0 t =
+let kill_dummy_args ids r t =
   let m = List.length ids in
   let bl = List.rev_map sign_of_id ids in
+  let rec found n = function
+    | MLrel r' when r' = r + n -> true
+    | MLmagic e -> found n e
+    | _ -> false
+  in
   let rec killrec n = function
-    | MLapp(e, a) when e = ast_lift n t0 ->
+    | MLapp(e, a) when found n e ->
 	let k = max 0 (m - (List.length a)) in
 	let a = List.map (killrec n) a in
 	let a = List.map (ast_lift k) a in
 	let a = select_via_bl bl (a @ (eta_args k)) in
 	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
-    | e when e = ast_lift n t0 ->
+    | e when found n e ->
 	let a = select_via_bl bl (eta_args m) in
 	named_lams ids (MLapp (ast_lift m e, a))
     | e -> ast_map_lift killrec n e
@@ -1031,28 +1050,28 @@ let rec kill_dummy = function
   | MLfix(i,fi,c) ->
       (try
 	 let ids,c = kill_dummy_fix i c in
-	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1))
+	 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids 1 (MLrel 1))
        with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
   | MLapp (MLfix (i,fi,c),a) ->
       let a = List.map kill_dummy a in
       (try
 	 let ids,c = kill_dummy_fix i c in
 	 let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in
-	 let fake' = kill_dummy_args ids (MLrel 1) fake in
+	 let fake' = kill_dummy_args ids 1 fake in
 	 ast_subst (MLfix (i,fi,c)) fake'
        with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a))
   | MLletin(id, MLfix (i,fi,c),e) ->
       (try
 	 let ids,c = kill_dummy_fix i c in
-	 let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in
+	 let e = kill_dummy (kill_dummy_args ids 1 e) in
 	 MLletin(id, MLfix(i,fi,c),e)
       with Impossible ->
 	MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
   | MLletin(id,c,e) ->
       (try
 	 let ids,c = kill_dummy_lams (kill_dummy_hd c) in
-	 let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in
-	 let c = eta_red (kill_dummy c) in
+	 let e = kill_dummy (kill_dummy_args ids 1 e) in
+	 let c = kill_dummy c in
 	 if is_atomic c then ast_subst c e else MLletin (id, c, e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
   | a -> ast_map kill_dummy a
@@ -1064,8 +1083,8 @@ and kill_dummy_hd = function
   | MLletin(id,c,e) ->
       (try
 	 let ids,c = kill_dummy_lams (kill_dummy_hd c) in
-	 let e = kill_dummy_hd (kill_dummy_args ids (MLrel 1) e) in
-	 let c = eta_red (kill_dummy c) in
+	 let e = kill_dummy_hd (kill_dummy_args ids 1 e) in
+	 let c = kill_dummy c in
 	 if is_atomic c then ast_subst c e else MLletin (id, c, e)
        with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e))
   | a -> a
@@ -1075,7 +1094,7 @@ and kill_dummy_fix i c =
   let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in
   let c = Array.copy c in c.(i) <- ci;
   for j = 0 to (n-1) do
-    c.(j) <- kill_dummy (kill_dummy_args ids (MLrel (n-i)) c.(j))
+    c.(j) <- kill_dummy (kill_dummy_args ids (n-i) c.(j))
   done;
   ids,c
 
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 6b0cd4f9..54a1baaa 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.mli 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: mlutil.mli 14786 2011-12-10 12:55:19Z letouzey $ i*)
 
 open Util
 open Names
@@ -30,6 +30,8 @@ val needs_magic : ml_type * ml_type -> bool
 val put_magic_if : bool -> ml_ast -> ml_ast
 val put_magic : ml_type * ml_type -> ml_ast -> ml_ast
 
+val generalizable : ml_ast -> bool
+
 (*s ML type environment. *)
 
 module Mlenv : sig
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 23ec108a..ffa38def 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.ml 14006 2011-04-14 23:09:56Z letouzey $ i*)
+(*i $Id: modutil.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Declarations
@@ -66,7 +66,7 @@ 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
+  | Record l -> List.iter (Option.iter do_term) l
   | _ -> ()
 
 let type_iter_references do_type t =
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index bb405d60..26d07872 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: modutil.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Declarations
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 81eea9e2..c07a1758 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
+(*i $Id: ocaml.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*s Production of Ocaml syntax. *)
 
@@ -113,9 +113,18 @@ let get_infix r =
   let s = find_custom r in
   String.sub s 1 (String.length s - 2)
 
-exception NoRecord
+let get_ind = function
+  | IndRef _ as r -> r
+  | ConstructRef (ind,_) -> IndRef ind
+  | _ -> assert false
 
-let find_projections = function Record l -> l | _ -> raise NoRecord
+let pp_one_field r i = function
+  | Some r -> pp_global Term r
+  | None -> pp_global Type (get_ind r) ++ str "__" ++ int i
+
+let pp_field r fields i = pp_one_field r i (List.nth fields i)
+
+let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
@@ -202,9 +211,9 @@ let rec pp_expr par env args =
     | MLcons (_,r,[]) ->
 	assert (args=[]);
 	pp_global Cons r
-    | MLcons ({c_kind = Record projs}, r, args') ->
+    | MLcons ({c_kind = Record fields}, r, args') ->
 	assert (args=[]);
-	pp_record_pat (projs, List.map (pp_expr true env []) args')
+	pp_record_pat (pp_fields r fields, List.map (pp_expr true env []) args')
     | MLcons (_,r,[arg1;arg2]) when is_infix r ->
 	assert (args=[]);
 	pp_par par
@@ -234,25 +243,25 @@ let rec pp_expr par env args =
 	  (pp_expr false env [] t)
 	in
 	(try
-	   let projs = find_projections info.m_kind in
-	   let (_, ids, c) = pv.(0) in
+	   (* First, can this match be printed as a mere record projection ? *)
+	   let fields =
+	     match info.m_kind with Record f -> f | _ -> raise Impossible
+	   in
+	   let (r, ids, c) = pv.(0) in
 	   let n = List.length ids in
+	   let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
+	   let proj_hd i =
+	     pp_expr true env [] t ++ str "." ++ pp_field r fields i
+	   in
 	   match c with
-	     | MLrel i when i <= n ->
-		 apply (pp_par par' (pp_expr true env [] t ++ str "." ++
-				     pp_global Term (List.nth projs (n-i))))
-	     | MLapp (MLrel i, a) when i <= n ->
-		 if List.exists (ast_occurs_itvl 1 n) a
-		 then raise NoRecord
-		 else
-		   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env
-		   in
-		   (pp_apply
-		      (pp_expr true env [] t ++ str "." ++
-		       pp_global Term (List.nth projs (n-i)))
-		      par ((List.map (pp_expr true env' []) a) @ args))
-	     | _ -> raise NoRecord
-	 with NoRecord ->
+	     | MLrel i when i <= n -> apply (pp_par par' (proj_hd (n-i)))
+	     | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) ->
+	       let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
+	       (pp_apply (proj_hd (n-i))
+		  par ((List.map (pp_expr true env' []) a) @ args))
+	     | _ -> raise Impossible
+	 with Impossible ->
+	   (* Second, can this match be printed as a let-in ? *)
 	   if Array.length pv = 1 then
 	     let s1,s2 = pp_one_pat env info pv.(0) in
 	     apply
@@ -263,6 +272,7 @@ let rec pp_expr par env args =
 			 ++ spc () ++ str "in") ++
 		      spc () ++ hov 0 s2)))
 	   else
+	     (* Otherwise, standard match *)
  	     apply
       	       (pp_par par'
 		  (try pp_ifthenelse par' env expr pv
@@ -283,11 +293,11 @@ let rec pp_expr par env args =
 	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
 
 
-and pp_record_pat (projs, args) =
+and pp_record_pat (fields, args) =
    str "{ " ++
    prlist_with_sep (fun () -> str ";" ++ spc ())
-     (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a)
-     (List.combine projs args) ++
+     (fun (f,a) -> f ++ str " =" ++ spc () ++ a)
+     (List.combine fields args) ++
    str " }"
 
 and pp_ifthenelse par env expr pv = match pv with
@@ -304,18 +314,18 @@ and pp_ifthenelse par env expr pv = match pv with
 and pp_one_pat env info (r,ids,t) =
   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
   let expr = pp_expr (expr_needs_par t) env' [] t in
-  try
-    let projs = find_projections info.m_kind in
-    pp_record_pat (projs, List.rev_map pr_id ids), expr
-  with NoRecord ->
-    (match List.rev ids with
-      | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
-      | [] -> pp_global Cons r
-      | ids ->
+  let patt = match info.m_kind with
+    | Record fields ->
+      pp_record_pat (pp_fields r fields, List.rev_map pr_id ids)
+    | _ -> match List.rev ids with
+	| [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
+	| [] -> pp_global Cons r
+	| ids ->
 	  (* hack Extract Inductive prod *)
 	  (if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ())
-	   ++ pp_boxed_tuple pr_id ids),
-    expr
+	  ++ pp_boxed_tuple pr_id ids
+  in
+  patt, expr
 
 and pp_pat env info pv =
   let factor_br, factor_set = try match info.m_same with
@@ -448,10 +458,11 @@ let pp_singleton kn packet =
 	 pp_comment (str "singleton inductive, whose constructor was " ++
 		     pr_id packet.ip_consnames.(0)))
 
-let pp_record kn projs ip_equiv packet =
-  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
-  let projnames = List.map (pp_global Term) projs in
-  let l = List.combine projnames packet.ip_types.(0) in
+let pp_record kn fields ip_equiv packet =
+  let ind = IndRef (mind_of_kn kn,0) in
+  let name = pp_global Type ind in
+  let fieldnames = pp_fields ind fields in
+  let l = List.combine fieldnames packet.ip_types.(0) in
   let pl = rename_tvars keywords packet.ip_vars in
   str "type " ++ pp_parameters pl ++ name ++
   pp_equiv pl name ip_equiv ++ str " = { "++
@@ -512,8 +523,7 @@ let pp_mind kn i =
   match i.ind_kind with
     | Singleton -> pp_singleton kn i.ind_packets.(0)
     | Coinductive -> pp_ind true kn i
-    | Record projs ->
-	pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0)
+    | Record fields -> pp_record kn fields (i.ind_equiv,0) i.ind_packets.(0)
     | Standard -> pp_ind false kn i
 
 let pp_decl = function
diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index 477b4351..c0b4e5b3 100644
--- a/plugins/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: ocaml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 val ocaml_descr : Miniml.language_descr
 
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index cb980cba..1f04ca59 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.ml 14006 2011-04-14 23:09:56Z letouzey $ i*)
+(*i $Id: scheme.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*s Production of Scheme syntax. *)
 
diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli
index e413d31e..c7c3d8b5 100644
--- a/plugins/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
@@ -1,11 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: scheme.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 val scheme_descr : Miniml.language_descr
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index b2b5e6f5..67cf2210 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml 14012 2011-04-15 16:45:27Z letouzey $ i*)
+(*i $Id: table.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Term
@@ -21,10 +21,21 @@ open Util
 open Pp
 open Miniml
 
-(** Sets and maps for [global_reference] that do _not_ work modulo
-    name equivalence (otherwise use Refset / Refmap ) *)
+(** Sets and maps for [global_reference] that work modulo equivalent
+    on the user part of the name (otherwise use Refset / Refmap ) *)
+
+module RefOrd = struct
+  type t = global_reference
+  let compare x y =
+    let make_name = function
+      | ConstRef con -> ConstRef(constant_of_kn(user_con con))
+      | IndRef (kn,i) -> IndRef(mind_of_kn(user_mind kn),i)
+      | ConstructRef ((kn,i),j)-> ConstructRef((mind_of_kn(user_mind kn),i),j)
+      | VarRef id -> VarRef id
+    in
+    Pervasives.compare (make_name x) (make_name y)
+end
 
-module RefOrd = struct type t = global_reference let compare = compare end
 module Refmap' = Map.Make(RefOrd)
 module Refset' = Set.Make(RefOrd)
 
@@ -316,6 +327,15 @@ let error_no_module_expr mp =
        ++ str "some Declare Module outside any Module Type.\n"
        ++ str "This situation is currently unsupported by the extraction.")
 
+let error_singleton_become_prop id =
+  err (str "The informative inductive type " ++ pr_id id ++
+       str " has a Prop instance.\n" ++
+       str "This happens when a sort-polymorphic singleton inductive type\n" ++
+       str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
+       str "The Ocaml extraction cannot handle this situation yet.\n" ++
+       str "Instead, use a sort-monomorphic type such as (True /\\ True)\n" ++
+       str "or extract to Haskell.")
+
 let error_unknown_module m =
   err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
 
@@ -335,10 +355,6 @@ let error_MPfile_as_mod mp b =
 	    "Monolithic Extraction cannot deal with this situation.\n"^
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
-let error_record r =
-  err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
-       fnl () ++ str "To help extraction, please use an explicit name.")
-
 let msg_non_implicit r n id =
   let name = match id with
     | Anonymous -> ""
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 2eafe1d8..b70d3efa 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.mli 14012 2011-04-15 16:45:27Z letouzey $ i*)
+(*i $Id: table.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Libnames
@@ -30,11 +30,11 @@ val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : module_path -> module_path -> 'a
 val error_no_module_expr : module_path -> 'a
+val error_singleton_become_prop : identifier -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
 val error_MPfile_as_mod : module_path -> bool -> 'a
-val error_record : global_reference -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit