Minor removals (#3786)

Found while working on parser migration of datatypes.

diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index b2399472ab143e74948446b2463e9d655ee8d687..08fe9965bfff8f8120078691046fcc8fc5eb544d 100644 (file)
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -243,9 +243,6 @@ class DType
   /** is this a tuple datatype? */
   bool isTuple() const;
 
-  /** get the record representation for this datatype */
-  Record* getRecord() const;
-
   /**
    * Return the cardinality of this datatype.
    * The DType must be resolved.

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index e11ac67f135157f0c9f5faa399c1e89c0bc0b7da..0779fdc58bf1340812a8a2867bce3ee9b3c81720 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -24,19 +24,9 @@
 #include "theory/datatypes/theory_datatypes_utils.h"
 
 namespace CVC4 {
-
-namespace expr {
-namespace attr {
-struct DatatypeConstructorTypeGroundTermTag {};
-} /* CVC4::expr::attr namespace */
-} /* CVC4::expr namespace */
-
 namespace theory {
 namespace datatypes {
 
-typedef expr::Attribute<expr::attr::DatatypeConstructorTypeGroundTermTag, Node>
-    GroundTermAttr;
-
 struct DatatypeConstructorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
                                      bool check) {