From 94a60883751530f0867e2ef3c0aec87f848033dc Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 5 Dec 2016 14:28:23 +0100
Subject: [PATCH] Update some documentation
---
src/main/scala/inox/ast/Expressions.scala | 7 ++-----
src/main/scala/inox/ast/Paths.scala | 4 ++--
2 files changed, 4 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 5f1fd53fa..aff201f83 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -30,7 +30,7 @@ trait Expressions { self: Trees =>
}
}
- /** Represents an expression in Leon. */
+ /** Represents an expression in Inox. */
abstract class Expr extends Tree with Typed
/** Trait which gets mixed-in to expressions without subexpressions */
@@ -326,9 +326,6 @@ trait Expressions { self: Trees =>
}
/** $encodingof `... ==> ...` (logical implication).
- *
- * This is not a standard Scala operator, but it results from an implicit
- * conversion in the Leon library.
*
* @see [[Constructors.implies]]
*/
@@ -428,7 +425,7 @@ trait Expressions { self: Trees =>
*
* Division and Remainder follows Java/Scala semantics. Division corresponds
* to / operator on BigInt and Remainder corresponds to %. Note that in
- * Java/Scala % is called remainder and the "mod" operator (Modulo in Leon) is also
+ * Java/Scala % is called remainder and the "mod" operator (Modulo in Inox) is also
* defined on BigInteger and differs from Remainder. The "mod" operator
* returns an always positive remainder, while Remainder could return
* a negative remainder. The following must hold:
diff --git a/src/main/scala/inox/ast/Paths.scala b/src/main/scala/inox/ast/Paths.scala
index 6e15804d1..2035fd878 100644
--- a/src/main/scala/inox/ast/Paths.scala
+++ b/src/main/scala/inox/ast/Paths.scala
@@ -128,7 +128,7 @@ trait Paths { self: SymbolOps with TypeOps with Constructors =>
* within a fixpoint computation where the `ids` set is iteratively computed
* by performing [[filterByIds]] calls on some (unchaning) base [[Path]].
*
- * @see [[leon.purescala.FunctionClosure.close]] for an example usecase.
+ * @see [[stainless.extraction.innerfuns.FunctionClosure.transform]] for an example usecase.
*/
def filterByIds(ids: Set[Identifier]): Path = {
def containsIds(ids: Set[Identifier])(e: Expr): Boolean = exprOps.exists {
@@ -216,7 +216,7 @@ trait Paths { self: SymbolOps with TypeOps with Constructors =>
lazy val toClause: Expr = and(BooleanLiteral(true))
/** Like [[toClause]] but doesn't simplify final path through constructors
- * from [[leon.purescala.Constructors]] */
+ * from [[Constructors]] */
lazy val fullClause: Expr = fold[Expr](BooleanLiteral(true), Let, And(_, _))(elements)
/** Folds the path into a boolean proposition where let-bindings are
--
GitLab