aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-06-02 16:11:03 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2016-06-02 16:13:30 +0200
commit9907e296e21fdd9dc3fab2b84fe7159b35af654c (patch)
treefc57dc4b3c6827655d3ce691248411838ace628b /kernel
parent2d2d86c165cac7b051da1c5079d614a76550a20c (diff)
Remove tabulation support from pretty-printing.
This mechanism relied on functions that are deprecated in recent versions of ocaml. It was incorrectly used for the most part anyway. The only place that was using tabulations correctly is "print_loadpath", so there is a minor regression there: physical paths of short logical paths are no longer aligned.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index a705e3004..09afbb575 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -278,7 +278,7 @@ and pp_bytecodes c =
| Ksequence (l1, l2) :: c ->
pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c
| i :: c ->
- tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
+ pp_instr i ++ fnl () ++ pp_bytecodes c
(*spiwack: moved this type in this file because I needed it for
retroknowledge which can't depend from cbytegen *)