Annotate correctly

epfl-lara · Aug 24, 2015 · fcac011 · fcac011
1 parent 63ff8d3
commit fcac011
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/library/lang/Rational.scala b/library/lang/Rational.scala
@@ -82,6 +82,7 @@ case class Rational(numerator: BigInt, denominator: BigInt) {
   }
 }
 
+@library
 object Rational {
 
   implicit def bigIntToRat(n: BigInt): Rational = Rational(n, 1)

diff --git a/library/proof/Internal.scala b/library/proof/Internal.scala
@@ -5,11 +5,10 @@ import leon.lang._
 import leon.annotation._
 
 /** Internal helper classes and methods for the 'proof' package. */
-@library
 object Internal {
 
   /*** Helper classes for relational reasoning ***/
-
+  @library
   case class WithRel[A, B](x: A, r: (A, B) => Boolean, prop: Boolean) {
 
     /** Continue with the next relation. */
@@ -33,6 +32,7 @@ object Internal {
     def qed: Boolean = prop
   }
 
+  @library
   case class WithProof[A, B](
     x: A, r: (A, B) => Boolean, proof: Boolean, prop: Boolean) {