diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-10 01:46:22 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-10 01:46:22 +0000 |
| commit | 1347a59b1198dabbcb6e8a697d896804d533c8d3 (patch) | |
| tree | 89d4d59bfc662293027400c48e21043556c489fb | |
| parent | dc8dfc8e47e51f0407f5b678e645897a83cc9754 (diff) | |
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
| -rw-r--r-- | contrib/extraction/common.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 48e169f70..150fb8fae 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 *) |