diff --git a/src/main/scala/inox/ast/Trees.scala b/src/main/scala/inox/ast/Trees.scala index 7b0f89a1aefeecce12ff25b3b959d7c068ef172d..272ff38c5fb3035874e23dee9f2a8822b10577e0 100644 --- a/src/main/scala/inox/ast/Trees.scala +++ b/src/main/scala/inox/ast/Trees.scala @@ -15,21 +15,6 @@ trait Trees with Printers with TreeOps { - /** We provide aliases to [[ast.Identifier]] and [[ast.FreshIdentifier]] here in - * order for {{{import trees._}}} to also provide these. Note that this DOES NOT - * mean that [[Identifier]] or [[FreshIdentifier]] become dependent types!! - * - * I (@nv) feel it makes sense for all types necessary for expression/tree - * construction to be available from a single import. It would be rather - * counter-intuitive for an Inox user to have to go in search of the - * [[ast.Identifier]] type in the [[ast]] package when all other expression and - * definitions have been imported. - */ - type Identifier = ast.Identifier - - /** @see [[Identifier]] for a discussion about why this is here. */ - val FreshIdentifier = ast.FreshIdentifier - class Unsupported(t: Tree, msg: String)(implicit ctx: Context) extends Exception(s"${t.asString(PrinterOptions.fromContext(ctx))}@${t.getPos} $msg") diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala index 6b9220f401a1874243e926378731c9a36372eeaf..3f22606184759fa1f4721bc0921970e7cfce7eef 100644 --- a/src/main/scala/inox/package.scala +++ b/src/main/scala/inox/package.scala @@ -1,7 +1,5 @@ /* Copyright 2009-2016 EPFL, Lausanne */ -import inox.ast.Identifier - /** Core package of the Inox solving interface * * == Structure == @@ -23,6 +21,18 @@ package object inox { case class FatalError(msg: String) extends Exception(msg) + /** We provide aliases to [[ast.Identifier]] and [[ast.FreshIdentifier]] here + * for a more natural import experience. + * + * Indeed, as Inox typically follows a pattern of nesting package clauses with + * the outer-most being {{{package inox}}}, including these basic definitions + * in the default imports makes my (@nv) life easier. + */ + type Identifier = ast.Identifier + + /** @see [[Identifier]] for why this is here */ + val FreshIdentifier = ast.FreshIdentifier + type InoxProgram = Program { val trees: inox.trees.type } object InoxProgram {