aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/pretty.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 6e831dc286..ba012d5202 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -100,7 +100,7 @@ let print_mutual sp mib =
array_map2 (fun id c -> (id, snd (decomp_n_prod env evd nparams c)))
(mis_consnames mis) lC in
let plidC =
- prvect_with_sep (fun () -> [<'bRK(1,0); 'sTR "| " >])
+ prvect_with_sep (fun () -> [<'bRK(0,0); 'sTR "| " >])
pr_constructor
lidC
in