diff options
Diffstat (limited to 'debugger/printval.ml')
| -rw-r--r-- | debugger/printval.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/debugger/printval.ml b/debugger/printval.ml index 4fa3055b0..0e37bad6b 100644 --- a/debugger/printval.ml +++ b/debugger/printval.ml @@ -15,8 +15,6 @@ (* To print values *) -open Misc -open Obj open Format open Parser_aux open Path |