summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-09-18 11:17:52 -0500
committerGitHub <noreply@github.com>2019-09-18 11:17:52 -0500
commit49bfeaad5a19bc86a3354681e19edd6ad3210795 (patch)
tree0326f129bb1dd776f777450cbf6e63c3f8796e9a
parent2bb23eca6e3a239c33f5f4eb2dd0056de0738686 (diff)
Minor cleaning (#3295)
-rw-r--r--src/expr/expr_manager_template.cpp3
-rw-r--r--src/expr/expr_manager_template.h5
2 files changed, 1 insertions, 7 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 988705aa8..bc3d450d0 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -715,9 +715,6 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
(*i)->getName().c_str());
nameResolutions.insert(std::make_pair((*i)->getName(), dtt));
dtts.push_back(dtt);
- //d_keep_dtt.push_back(dtt);
- //d_keep_dt.push_back(*i);
- //Assert( dtt.getDatatype()==(*i) );
}
// Second, set up the type substitution map for complex type
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index a4efa7286..44871ff99 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -79,10 +79,7 @@ private:
// undefined, private copy constructor and assignment op (disallow copy)
ExprManager(const ExprManager&) = delete;
ExprManager& operator=(const ExprManager&) = delete;
-
- std::vector<DatatypeType> d_keep_dtt;
- std::vector<Datatype> d_keep_dt;
-
+
public:
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback