aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/pretty.ml8
1 files changed, 5 insertions, 3 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 2143178383..af94577af2 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -45,9 +45,11 @@ let print_impl_args = function
synthesizes the type nat of the abstraction on u *)
let print_named_def name body typ =
- [< 'sTR "*** ["; 'sTR name ; 'sPC;
- hOV 0 [< 'sTR ":="; 'sPC; prterm body; 'sPC;
- 'sTR ": "; prtype typ >];
+ let pbody = prterm body in
+ let ptyp = prtype typ in
+ [< 'sTR "*** ["; 'sTR name ; 'sTR " ";
+ hOV 0 [< 'sTR ":="; 'bRK (1,2); pbody; 'sPC;
+ 'sTR ":"; 'bRK (1,2); ptyp >];
'sTR "]"; 'fNL >]
let print_named_assum name typ =