fix(library/blast/backward): crash when pretty printing backward rule set

We make sure it doesn't depend on the blast state.

src/library/blast/backward/backward_rule_set.cpp

@@ -90,7 +90,7 @@ backward_rule_set get_backward_rule_sets(environment const & env, options const
 io_state_stream const & operator<<(io_state_stream const & out, backward_rule_set const & brs) {
     out << "backward rules\n";
     brs.for_each([&](head_index const & head_idx, backward_rule const & r) {
-            out << head_idx << " ==> " << r.get_proof() << "\n";
+            out << head_idx << " ==> " << r.get_proof().to_bare_expr() << "\n";
         });
     return out;
 }

src/library/blast/gexpr.h

@@ -42,6 +42,9 @@ public:
         create fresh universe meta-variables */
     expr to_expr() const;
 
+    /** \brief Return "bare" expression (without adding fresh metavariables if universe polymorphic) */
+    expr to_bare_expr() const { return m_expr; }
+
     friend bool operator==(gexpr const & ge1, gexpr const & ge2);
     friend std::ostream const & operator<<(std::ostream const & out, gexpr const & ge);
 };

tests/lean/backward_rule1.lean.expected.out

@@ -2,8 +2,8 @@ constant H [backward] : A → B
 constant G [backward] : A → B → C
 constant f [backward] : T → A
 backward rules
-exists_unique ==> exists_unique.intro (poly)
+exists_unique ==> exists_unique.intro
 B ==> H
-A ==> f (poly)
+A ==> f
 C ==> G
-Exists ==> Exists.intro (poly)
+Exists ==> Exists.intro