diff options
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 |