From fcac0116fc692bd7892f8ce2a9c7c883b6850dda Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 24 Aug 2015 17:13:10 +0200
Subject: [PATCH] Annotate correctly

---
 library/lang/Rational.scala  | 1 +
 library/proof/Internal.scala | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/lang/Rational.scala b/library/lang/Rational.scala
index c8027dee9..f4a10215b 100644
--- 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
index 72333c501..ad395f532 100644
--- 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) {
 
-- 
GitLab