diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/common.ml | 10 | ||||
| -rw-r--r-- | contrib/extraction/extract_env.ml | 17 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.ml | 4 |
3 files changed, 17 insertions, 14 deletions
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 |