From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 20 Feb 2020 19:07:22 +0000 (-0600)
Subject: Minor removals (#3786)
X-Git-Tag: cvc5-1.0.0~3628
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c780b1778e97afe15a0eb2522505b796cd5bbe71;p=cvc5.git

Minor removals (#3786)

Found while working on parser migration of datatypes.
---

diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index b2399472a..08fe9965b 100644
--- 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 e11ac67f1..0779fdc58 100644
--- 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) {