diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index c312ad18fe6000ab5f583ab131ebe26de5ecb5d5..41f469eaeeff441c7e6958ab16f555406b8d99d8 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -148,8 +148,16 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
     
   }
   
-  def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = tree match {
-    
+  def pp(tree: Tree)(implicit ctx: PrinterContext): Unit = {
+    if (opts.printTypes) {
+      tree match {
+        case t: Expr =>
+          p"⟨"
+
+        case _ =>
+      }
+    }
+    tree match {
       case id: Identifier =>
         
         val name = if (opts.printUniqueIds) {
@@ -657,7 +665,15 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
       case (tree: PrettyPrintable) => tree.printWith(ctx)
 
       case _ => sb.append("Tree? (" + tree.getClass + ")")
-    
+    }
+    if (opts.printTypes) {
+      tree match {
+        case t: Expr=>
+          p" : ${t.getType} ⟩"
+
+        case _ =>
+      }
+    }
   }
 
   object FcallMethodInvocation {
diff --git a/src/main/scala/leon/purescala/PrinterOptions.scala b/src/main/scala/leon/purescala/PrinterOptions.scala
index 0a9cb6d771f78cf1f4bdc1921972caf1164069ae..6a95b265d7871df9c5575a2ea605e457097b4e3f 100644
--- a/src/main/scala/leon/purescala/PrinterOptions.scala
+++ b/src/main/scala/leon/purescala/PrinterOptions.scala
@@ -8,20 +8,21 @@ import utils._
 case class PrinterOptions (
   baseIndent: Int = 0,
   printPositions: Boolean = false,
-  printTypes: Boolean = false,
-  printUniqueIds: Boolean = false
+  printUniqueIds: Boolean = false,
+  printTypes: Boolean = false
 )
 
 object PrinterOptions {
   def fromContext(ctx: LeonContext): PrinterOptions = {
     val debugTrees     = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTrees
+    val debugTypes     = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionTypes
     val debugPositions = ctx.findOptionOrDefault(SharedOptions.optDebug) contains DebugSectionPositions
 
     PrinterOptions(
       baseIndent     = 0,
       printPositions = debugPositions,
-      printTypes     = debugTrees,
-      printUniqueIds = debugTrees
+      printUniqueIds = debugTrees,
+      printTypes     = debugTypes
     )
   }
 }
diff --git a/src/main/scala/leon/utils/DebugSections.scala b/src/main/scala/leon/utils/DebugSections.scala
index 7562edf59a4aca0cb62d9bf8099376619524ab6f..9ccabc241de2e1a03dfa49246b944406a550a49f 100644
--- a/src/main/scala/leon/utils/DebugSections.scala
+++ b/src/main/scala/leon/utils/DebugSections.scala
@@ -21,6 +21,7 @@ case object DebugSectionEvaluation   extends DebugSection("eval",         1 << 9
 case object DebugSectionRepair       extends DebugSection("repair",       1 << 10)
 case object DebugSectionLeon         extends DebugSection("leon",         1 << 11)
 case object DebugSectionXLang        extends DebugSection("xlang",        1 << 12)
+case object DebugSectionTypes        extends DebugSection("types",        1 << 13)
 
 object DebugSections {
   val all = Set[DebugSection](
@@ -36,6 +37,7 @@ object DebugSections {
     DebugSectionEvaluation,
     DebugSectionRepair,
     DebugSectionLeon,
-    DebugSectionXLang
+    DebugSectionXLang,
+    DebugSectionTypes
   )
 }