diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index c764f6cb1..8b7fe8785 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -38,6 +38,7 @@ private: public: typedef unsynch_mpq_manager numeral_manager; typedef bound_deps deps_combine_rule; + typedef deps_combine_rule interval_deps_combine_rule; struct interval { interval() :