diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-23 16:31:04 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-23 16:31:04 +0000 |
| commit | 68da8bd15b9e8d7bfae0baa21195d6f1e6b93311 (patch) | |
| tree | 34af94a3c172d3f1b294f723787f6c43367da764 /plugins | |
| parent | e2218904bccbfca92fbf39ec55c0766874dfa5b8 (diff) | |
Extraction: nicer simple extraction of custom defs (fix #2204)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13192 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 33bac0e1c..7a82b3567 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -480,15 +480,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 |