Commit 2020-04-07 06:44 c85453d9

fix(tactic/refine_struct): don't add unnecessary eq.mpr or id (#2319)

• fix(tactic/interactive): don't unfold non-Prop goals The old behaviour caused eq.mpr's in pi_instance output.
• add a test file
• move test
• actually move test
• Update test/refine_struct.lean
• test: fix compile
• Apply suggestions from code review Co-Authored-By: Gabriel Ebner gebner@gebner.org
• Try a fix by @gebner and @cipher1024
• Update test/refine_struct.lean Co-Authored-By: Gabriel Ebner gebner@gebner.org
• apply Gabriel's suggestion