diff --git a/build.sbt b/build.sbt
index 6517cf1e6f24679d60aef375c7dcf1577739779b..5b984ed01dc07a99e12adf882198d16d2a667043 100644
--- a/build.sbt
+++ b/build.sbt
@@ -91,7 +91,7 @@ sourceGenerators in Compile <+= Def.task {
   IO.write(build, s"""|package leon
                       |
                       |object Build {
-                      |  val baseDirectory = \"${baseDirectory.value.toString}\"
+                      |  val baseDirectory = \"\"\"${baseDirectory.value.toString}\"\"\"
                       |  val libFiles = List(
                       |    ${libFiles.mkString("\"\"\"", "\"\"\",\n    \"\"\"", "\"\"\"")}
                       |  )
diff --git a/library/lang/Either.scala b/library/lang/Either.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9cc2ea4e9537b424cbce6963e2a4038f3480d01a
--- /dev/null
+++ b/library/lang/Either.scala
@@ -0,0 +1,27 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package leon.lang
+
+import leon.annotation._
+
+/**
+ * @author Viktor
+ */
+@library
+sealed abstract class Either[A,B] {
+  def isLeft : Boolean
+  def isRight : Boolean
+  def swap : Either[B,A]
+}
+@library
+case class Left[A,B](content: A) extends Either[A,B] {
+  def isLeft = true
+  def isRight = false
+  def swap = Right[B,A](content)
+}
+@library
+case class Right[A,B](content: B) extends Either[A,B] {
+  def isLeft = false
+  def isRight = true
+  def swap = Left[B,A](content)
+}
\ No newline at end of file
diff --git a/src/main/scala/leon/utils/SCC.scala b/src/main/scala/leon/utils/SCC.scala
index d451accf70c817d243a4355e696cd7e9e00e91e3..dbde69fc1e03b3a0e6655806b75c09fec93003bf 100644
--- a/src/main/scala/leon/utils/SCC.scala
+++ b/src/main/scala/leon/utils/SCC.scala
@@ -3,8 +3,11 @@
 package leon
 package utils
 
-/** This could be defined anywhere, it's just that the
-    termination checker is the only place where it is used. */
+/** Returns the list of strongly connected sets of vertices.
+  * A set is said strongly connected is from any vertex we can reach another vertex transitively.
+  *  
+  * This could be defined anywhere, it's just that the
+  * termination checker is the only place where it is used. */
 object SCC {
   def scc[T](graph : Map[T,Set[T]]) : List[Set[T]] = {
     // The first part is a shameless adaptation from Wikipedia