feat(library/unifier): 'forget' justifications after finding a solution, the justifications are only needed inside the unifier (for implementing nonchronological backtracking)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/metavar.h

@@ -60,6 +60,9 @@ public:
     void d_assign(level const & m, level const & t, justification const & j) { d_assign(meta_id(m), t, j); }
     void d_assign(level const & m, level const & t) { d_assign(m, t, justification ()); }
 
+    void d_forget_justifications() { m_expr_jsts  = jst_map(); m_level_jsts = jst_map(); }
+    substitution forget_justifications() const { substitution s(*this); s.d_forget_justifications(); return s; }
+
     template<typename F>
     void for_each_expr(F && fn) const {
         for_each(m_expr_subst, [=](name const & n, expr const & e) { fn(n, e, get_expr_jst(n)); });

src/library/unifier.cpp

@@ -1156,7 +1156,7 @@ struct unifier_fn {
         }
         lean_assert(!in_conflict());
         lean_assert(m_cnstrs.empty());
-        return optional<substitution>(m_subst);
+        return optional<substitution>(m_subst.forget_justifications());
     }
 };