Applying same convention as in Definition for printing type in a let in.

Also adding spaces around ":=" and ":" when printed as "(x : t := c)".
Example:

Check fun y => let x : True := I in fun z => z+y=0.
(* λ (y : nat) (x : True := I) (z : nat), z + y = 0
     : nat → nat → Prop *)

2 files changed, 2 insertions, 2 deletions

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index ad60aeccce..1ec701ae81 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -32,7 +32,7 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
      : Type -> Prop
 λ A : Type, ∀ n p : A, n = p
      : Type -> Prop
-let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
+let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
      : bool -> nat
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
      : (nat -> nat) -> nat -> nat
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index 576fbd7c0b..e83e7176de 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,7 +6,7 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x := A n : T n in ?y ?y0 : T n
+fun n : nat => let x : T n := A n in ?y ?y0 : T n
      : forall n : nat, T n
 where
 ?y : [n : nat  x := A n : T n |- ?T -> T n]