diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
| commit | da178a880e3ace820b41d38b191d3785b82991f5 (patch) | |
| tree | 6356ab3164a5ad629f4161dc6c44ead74edc2937 /contrib/extraction/extract_env.ml | |
| parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) | |
Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg
Diffstat (limited to 'contrib/extraction/extract_env.ml')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 17 |
1 files changed, 7 insertions, 10 deletions
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 |