diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-27 15:30:11 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-27 15:30:11 +0000 |
| commit | 1e996160e916e2c8fc9288723a49e9045d4d1895 (patch) | |
| tree | 6ed9acd3de3816d99d10f5193a52a4c8dbc0dd4c | |
| parent | 169a08cf1656e5340d2833a8a7ca07ef25d740fb (diff) | |
dead code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10596 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/common.ml | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 7a6d42428..2be509954 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -480,16 +480,3 @@ let pp_module mp = error_module_clash base_s else dottify ls - -(*i - (* DO NOT REMOVE: used when making names resolution *) - let cout = open_out (f^".ren") in - let ft = Pp_control.with_output_to cout in - Hashtbl.iter - (fun r id -> - if short_module r = !current_module then - msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r))) - renamings; - pp_flush_with ft (); - close_out cout; -i*) |