make it fail

leanprover-community · Jan 7, 2023 · f9f19eb · f9f19eb
1 parent bbcaf3f
commit f9f19eb
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/tactic/hopt_param.lean b/src/tactic/hopt_param.lean
@@ -47,5 +47,5 @@ example : foo :=
   bar_eq := if_pos rfl }
 ``` -/
 meta def solve_default : command :=
-try_hopt_param <|> tactic.trace "A previous structure field was changed from its default value, so
+try_hopt_param <|> tactic.fail "A previous structure field was changed from its default value, so
   `solve_default` cannot solve the proof obligation automatically."