From 553116af166c9df0e8e5c6eadaa65929e061d417 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 10 Jun 2018 17:28:51 +0200
Subject: [PATCH] always split conjunctions in side-conditions

---
 theories/proofmode/ltac_tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 5e5ec2b3f..cd5655907 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 *)
 
-- 
GitLab