aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--parsing/pretty.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 6aaffa19df..152e2a50ac 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -45,9 +45,10 @@ 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 "="; prterm body; 'sPC; 'sTR ": "; prtype typ >] ;
- 'sTR "]"; 'fNL >]
+ [< 'sTR "*** ["; 'sTR name ; 'sPC;
+ hOV 0 [< 'sTR ":="; 'sPC; prterm body; 'sPC;
+ 'sTR ": "; prtype typ >];
+ 'sTR "]"; 'fNL >]
let print_named_assum name typ =
[< 'sTR "*** [" ; 'sTR name ; 'sTR " : "; prtype typ; 'sTR "]"; 'fNL >]