From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 1 Jul 2010 17:21:14 +0200
Subject: Imported Upstream version 8.2pl2+dfsg

---
 contrib/extraction/common.ml      | 10 ++++++++--
 contrib/extraction/extract_env.ml | 17 +++++++----------
 contrib/extraction/mlutil.ml      |  4 ++--
 3 files changed, 17 insertions(+), 14 deletions(-)

(limited to 'contrib/extraction')

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 02173c1f..73f44e68 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
+(*i $Id: common.ml 13200 2010-06-25 22:36:25Z letouzey $ i*)
 
 open Pp
 open Util
@@ -21,6 +21,8 @@ open Mlutil
 open Modutil
 open Mod_subst
 
+let string_of_id id = ascii_of_ident (Names.string_of_id id)
+
 (*s Some pretty-print utility functions. *)
 
 let pp_par par st = if par then str "(" ++ st ++ str ")" else st
@@ -73,7 +75,11 @@ let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
 let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
-let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
+let uppercase_id id =
+  let s = string_of_id id in
+  assert (s<>"");
+  if s.[0] = '_' then id_of_string ("Coq_"^s)
+  else id_of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 49a86200..057a7b29 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 11846 2009-01-22 18:55:10Z letouzey $ i*)
+(*i $Id: extract_env.ml 13201 2010-06-25 22:36:27Z letouzey $ i*)
 
 open Term
 open Declarations
@@ -489,15 +489,12 @@ let simple_extraction r = match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
       init false;
-      if is_custom r then
-	msgnl (str "User defined extraction:" ++ spc () ++
-		 str (find_custom r) ++ fnl ())
-      else
-	let struc = optimize_struct [r] (mono_environment [r] []) in
-	let d = get_decl_in_structure r struc in
-	warning_axioms ();
-	print_one_decl struc (modpath_of_r r) d;
-	reset ()
+      let struc = optimize_struct [r] (mono_environment [r] []) in
+      let d = get_decl_in_structure r struc in
+      warning_axioms ();
+      if is_custom r then msgnl (str "(** User defined extraction *)");
+      print_one_decl struc (modpath_of_r r) d;
+      reset ()
   | _ -> assert false
 
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 79aeea33..4e2904ba 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.ml 10329 2007-11-21 21:21:36Z letouzey $ i*)
+(*i $Id: mlutil.ml 13202 2010-06-25 22:36:30Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -578,7 +578,7 @@ let eta_red e =
 	  if m = n then 
 	    [], f, a
 	  else if m < n then 
-	    snd (list_chop (n-m) ids), f, a 
+	    list_skipn m ids, f, a
 	  else (* m > n *)
 	    let a1,a2 = list_chop (m-n) a in 
 	    [], MLapp (f,a1), a2
-- 
cgit v1.2.3