Commit 553116af authored by Ralf Jung's avatar Ralf Jung

always split conjunctions in side-conditions

parent 9af0d884
......@@ -44,7 +44,7 @@ Ltac iSolveTC :=
(** Tactic used for solving side-conditions arising from TC resolution in iMod
and iInv. *)
Ltac iSolveSideCondition :=
try (split_and?; solve [ fast_done | solve_ndisj ]).
split_and?; try solve [ fast_done | solve_ndisj ].
(** * Misc *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment