diff options
| author | letouzey | 2012-11-19 16:10:53 +0000 |
|---|---|---|
| committer | letouzey | 2012-11-19 16:10:53 +0000 |
| commit | 0d2b9721d0b4a58fb5ca0a4e0befa79c9ab2c1e7 (patch) | |
| tree | 79499e2a9f64520af91a523a6ab1ac91138def98 /lib | |
| parent | dab474813a7f8b02fe71c4aa47c49a25631ae5a3 (diff) | |
Serialize: dead code
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15985 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/serialize.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/lib/serialize.ml b/lib/serialize.ml index eb10bb4680..218372afc2 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -452,10 +452,6 @@ let to_message xml = match xml with { message_level = to_message_level lvl; message_content = to_string content } | _ -> raise Marshal_error -let of_hints = - let of_hint = of_list (of_pair of_string of_string) in - of_option (of_pair (of_list of_hint) of_hint) - let is_message = function | Element ("message", _, _) -> true | _ -> false |