diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v index 5e5ec2b3fffbafcadc3b201c38a754f3edcb4734..cd565590786eccd7228b18484c29e9749ad57a09 100644 --- a/theories/proofmode/ltac_tactics.v +++ b/theories/proofmode/ltac_tactics.v @@ -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 *)