diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-03 14:59:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-03 15:07:37 +0100 |
| commit | 281bed69ee7d4a7638d07f07f9d6722b897f29cc (patch) | |
| tree | 737464832cbc0a830371cb28c8002f0d34f8b140 /printing/ppconstr.ml | |
| parent | 6316e8b380a9942cd587f250eb4a69668e52019e (diff) | |
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
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index ea705e335..663b8b810 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 ) |