1 files changed, 4 insertions, 10 deletions
diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index c0a92214a..d6fe8ba0d 100644
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -25,8 +25,8 @@
 
 namespace cvc5 {
 
+class Env;
 class ProofNodeManager;
-class ResourceManager;
 class SmtEngine;
 class TConvProofGenerator;
 
@@ -47,7 +47,7 @@ struct SmtEngineStatistics;
 class ExpandDefs
 {
  public:
-  ExpandDefs(SmtEngine& smt, ResourceManager& rm, SmtEngineStatistics& stats);
+  ExpandDefs(SmtEngine& smt, Env& env, SmtEngineStatistics& stats);
   ~ExpandDefs();
   /**
    * Expand definitions in term n. Return the expanded form of n.
@@ -62,12 +62,6 @@ class ExpandDefs
       TNode n,
       std::unordered_map<Node, Node, NodeHashFunction>& cache,
       bool expandOnly = false);
-  /**
-   * Expand defintitions in assertions. This applies this above method to each
-   * assertion in the given pipeline.
-   */
-  void expandAssertions(preprocessing::AssertionPipeline& assertions,
-                        bool expandOnly = false);
 
   /**
    * Set proof node manager, which signals this class to enable proofs using the
@@ -87,8 +81,8 @@ class ExpandDefs
       TConvProofGenerator* tpg);
   /** Reference to the SMT engine */
   SmtEngine& d_smt;
-  /** Reference to resource manager */
-  ResourceManager& d_resourceManager;
+  /** Reference to the environment. */
+  Env& d_env;
   /** Reference to the SMT stats */
   SmtEngineStatistics& d_smtStats;
   /** A proof generator for the term conversion. */