5 files changed, 1 insertions, 27 deletions
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 93a0cbe99..d77981cc4 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -141,7 +141,6 @@ namespace CVC4 {
 %template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>;
 %template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>;
 %template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>;
-%template(getConstSubrangeBounds) CVC4::Expr::getConst<CVC4::SubrangeBounds>;
 %template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>;
 %template(getConstBitVectorExtract) CVC4::Expr::getConst<CVC4::BitVectorExtract>;
 %template(getConstBitVectorRotateLeft) CVC4::Expr::getConst<CVC4::BitVectorRotateLeft>;
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index b8f8d5da9..136e75f98 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -44,7 +44,6 @@
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorBitOf>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::SubrangeBounds>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRepeat>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorExtract>;
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateLeft>;
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 8719d8ef4..a12c68791 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -25,7 +25,6 @@
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "util/statistics.h"
-#include "util/subrange_bound.h"
 
 ${includes}
 
@@ -33,7 +32,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 36 "${template}"
 
 namespace CVC4 {
 
@@ -458,12 +457,6 @@ public:
   //Type mkPredicateSubtype(Expr lambda, Expr witness)
   //  throw(TypeCheckingException);
 
-  /**
-   * Make an integer subrange type as defined by the argument.
-   */
-  //Type mkSubrangeType(const SubrangeBounds& bounds)
-  //  throw(TypeCheckingException);
-
   /** Get the type of an expression */
   Type getType(Expr e, bool check = false)
     throw(TypeCheckingException);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f112381d8..fab5d4688 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -36,7 +36,6 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node_value.h"
-#include "util/subrange_bound.h"
 #include "options/options.h"
 
 namespace CVC4 {
diff --git a/src/expr/type.h b/src/expr/type.h
index 25f0c5436..dfab42dad 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -25,7 +25,6 @@
 #include <stdint.h>
 
 #include "util/cardinality.h"
-#include "util/subrange_bound.h"
 
 namespace CVC4 {
 
@@ -584,21 +583,6 @@ public:
   Type getParentType() const;
 
 };/* class PredicateSubtype */
-
-/**
- * Class encapsulating an integer subrange type.
- */
-class CVC4_PUBLIC SubrangeType : public Type {
-
-public:
-
-  /** Construct from the base type */
-  SubrangeType(const Type& type = Type()) throw(IllegalArgumentException);
-
-  /** Get the bounds defining this integer subrange */
-  SubrangeBounds getSubrangeBounds() const;
-
-};/* class SubrangeType */
 #endif /* 0 */
 
 /**