From 1347a59b1198dabbcb6e8a697d896804d533c8d3 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 10 Nov 2003 01:46:22 +0000
Subject: message informant de l'ecriture d'un fichier extrait

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4850 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/common.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 48e169f706..150fb8fae0 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -369,6 +369,10 @@ let print_one_decl struc mp decl =
 
 (*S Extraction to a file. *)
 
+let info f = 
+  Options.if_verbose msgnl 
+    (str ("The file "^f^" has been created by extraction."))
+
 let print_structure_to_file f prm struc =
   cons_cofix := Refset.empty;
   Hashtbl.clear renamings;
@@ -399,6 +403,7 @@ let print_structure_to_file f prm struc =
   with e -> 
     option_iter close_out cout; raise e
   end;
+  option_iter (fun (f,_) -> info f) f;
   (* print the signature *)
   match f with 
     | Some (_,f) when lang () = Ocaml -> 
@@ -410,8 +415,10 @@ let print_structure_to_file f prm struc =
 	  close_out cout;
 	with e -> 
 	  close_out cout; raise e 
-	end
-    | _ -> () 
+	end; 
+	info f 
+    | _ -> ()
+	  
 
 (*i 
   (* DO NOT REMOVE: used when making names resolution *)
-- 
cgit v1.2.3