aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/prettyp.ml5
-rw-r--r--parsing/printer.ml9
2 files changed, 11 insertions, 3 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index f781ff7558..5ccf11bdb3 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -97,7 +97,10 @@ let print_params env params =
if List.length params = 0 then
(mt ())
else
- (str "[" ++ pr_rel_context env params ++ str "]" ++ brk(1,2))
+ if !Options.v7 then
+ (str "[" ++ pr_rel_context env params ++ str "]" ++ brk(1,2))
+ else
+ (pr_rel_context env params ++ brk(1,2))
let rec contract_types = function
| [] -> []
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 06cec0db0b..fbae23c2d9 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -179,11 +179,16 @@ let pr_named_context_of env =
let pr_rel_context env rel_context =
let rec prec env = function
| [] -> (mt ())
- | [b] -> pr_rel_decl env b
+ | [b] ->
+ if !Options.v7 then pr_rel_decl env b
+ else str "(" ++ pr_rel_decl env b ++ str")"
| b::rest ->
let pb = pr_rel_decl env b in
let penvtl = prec (push_rel b env) rest in
- (pb ++ str";" ++ spc () ++ penvtl)
+ if !Options.v7 then
+ (pb ++ str";" ++ spc () ++ penvtl)
+ else
+ (str "(" ++ pb ++ str")" ++ spc () ++ penvtl)
in
prec env (List.rev rel_context)