"by j let x : T such that P(x)" generalized to allow arbitrary justifications.

[helm.git] / components / content_pres / termContentPres.ml

diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml
index a8bfe114746f5c9d79968d7c96141de6d8f27646..9f720e33b9a29740d414f6b5a0cd0d793ae0f2ef 100644 (file)
--- a/components/content_pres/termContentPres.ml
+++ b/components/content_pres/termContentPres.ml
@@ -199,9 +199,9 @@ let pp_ast0 t k =
         add_level_info Ast.let_in_prec Ast.let_in_assoc
           (hvbox false true [
             hvbox false true [
-              keyword "let";
+              keyword "let"; space;
               hvbox false true [
-                aux_var var; builtin_symbol "\\def"; break; top_pos (k s) ];
+                aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ];
               break; keyword "in" ];
             break;
             k t ])