diff options
| author | ppedrot | 2012-06-01 20:08:33 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-01 20:08:33 +0000 |
| commit | a92a0d051b987ba996905ccd4ce7ee3a5feb41c1 (patch) | |
| tree | ec5246ac1cfc741dc30c33fe6551216dfdef6a54 /plugins/extraction | |
| parent | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (diff) | |
More cleaning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index f107007363..4aa6eaa1c5 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -465,7 +465,7 @@ let print_structure_to_file (fn,si,mo) dry struc = (* First, a dry run, for computing objects to rename or duplicate *) set_phase Pre; let devnull = formatter true None in - msg_with devnull (d.pp_struct struc); + pp_with devnull (d.pp_struct struc); let opened = opened_libraries () in (* Print the implementation *) let cout = if dry then None else Option.map open_out fn in @@ -473,8 +473,8 @@ let print_structure_to_file (fn,si,mo) dry struc = begin try (* The real printing of the implementation *) set_phase Impl; - msg_with ft (d.preamble mo opened unsafe_needs); - msg_with ft (d.pp_struct struc); + pp_with ft (d.preamble mo opened unsafe_needs); + pp_with ft (d.pp_struct struc); Option.iter close_out cout; with e -> Option.iter close_out cout; raise e @@ -487,8 +487,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let ft = formatter false (Some cout) in begin try set_phase Intf; - msg_with ft (d.sig_preamble mo opened unsafe_needs); - msg_with ft (d.pp_sig (signature_of_structure struc)); + pp_with ft (d.sig_preamble mo opened unsafe_needs); + pp_with ft (d.pp_sig (signature_of_structure struc)); close_out cout; with e -> close_out cout; raise e |