fix(library/print): consider constant roots in is_used_name

src/library/print.cpp

@@ -19,7 +19,7 @@ bool is_used_name(expr const & t, name const & n) {
     bool found = false;
     for_each(t, [&](expr const & e, unsigned) {
             if (found) return false; // already found
-            if ((is_constant(e) && const_name(e) == n)  // t has a constant named n
+            if ((is_constant(e) && const_name(e).get_root() == n)  // t has a constant starting with n
                 || (is_local(e) && (mlocal_name(e) == n || local_pp_name(e) == n))) { // t has a local constant named n
                 found = true;
                 return false; // found it

tests/lean/pp_shadowed_const.lean

@@ -1 +1,4 @@
 def f : Π (x : nat) (b : bool), bool = bool := λ bool, _
+
+def g (heq : 1 == 1) := heq.symm
+#print g

tests/lean/pp_shadowed_const.lean.expected.out

@@ -2,3 +2,5 @@ pp_shadowed_const.lean:1:55: error: don't know how to synthesize placeholder
 context:
 bool : ℕ
 ⊢ _root_.bool → _root_.bool = _root_.bool
+def g : 1 == 1 → 1 == 1 :=
+λ (heq_1 : 1 == 1), heq.symm heq_1