From 281bed69ee7d4a7638d07f07f9d6722b897f29cc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 3 Dec 2015 14:59:27 +0100
Subject: Improving over printing of let-tuple (see #4447).

For instance, #4447 is now printed:

λ Ca Da : ℕAlg,
let (ℕ, ℕ0) := (Ca, Da) in
let (C, p) := ℕ in
let (c₀, cs) := p in
let (D, p0) := ℕ0 in
let (d₀, ds) := p0 in
{h : C → D & ((h c₀ = d₀) * (∀ c : C, h (cs c) = ds (h c)))%type}
     : ℕAlg → ℕAlg → Type
---
 printing/ppconstr.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ea705e335e..663b8b8101 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -638,13 +638,13 @@ end) = struct
       | CLetTuple (_,nal,(na,po),c,b) ->
         return (
           hv 0 (
-            keyword "let" ++ spc () ++
-              hov 0 (str "(" ++
+            hov 2 (keyword "let" ++ spc () ++
+              hov 1 (str "(" ++
                        prlist_with_sep sep_v pr_lname nal ++
                        str ")" ++
-                       pr_simple_return_type (pr mt) na po ++ str " :=" ++
-                       pr spc ltop c ++ spc ()
-                     ++ keyword "in") ++
+                       pr_simple_return_type (pr mt) na po ++ str " :=") ++
+                       pr spc ltop c
+                     ++ keyword " in") ++
               pr spc ltop b),
           lletin
         )
-- 
cgit v1.2.3