diff --git a/src/library/tactic/location.h b/src/library/tactic/location.h index 9366c607bd..b7f1fe3b30 100644 --- a/src/library/tactic/location.h +++ b/src/library/tactic/location.h @@ -61,9 +61,10 @@ private: kind m_kind; occurrence m_goal; list> m_hyps; - location(kind k, occurrence const & g = occurrence(), - list> const & hs = list>()): + location(kind k, occurrence const & g, list> const & hs): m_kind(k), m_goal(g), m_hyps(hs) {} + location(kind k, occurrence const & g):m_kind(k), m_goal(g) {} + location(kind k):location(k, occurrence()) {} public: location():m_kind(GoalOnly) {}