From 68da8bd15b9e8d7bfae0baa21195d6f1e6b93311 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 23 Jun 2010 16:31:04 +0000
Subject: 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
---
 plugins/extraction/extract_env.ml | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 33bac0e1c3..7a82b3567f 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
 
 
-- 
cgit v1.2.3