From b46797e03b53742b91aa547f7ede435983277938 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Tue, 26 Mar 2024 19:06:51 +0000
Subject: [PATCH] Drop unnecessary try

---
 SSA/Projects/Scf/ScfFunctor.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/SSA/Projects/Scf/ScfFunctor.lean b/SSA/Projects/Scf/ScfFunctor.lean
index 75ebfb15f..e82fd4026 100644
--- a/SSA/Projects/Scf/ScfFunctor.lean
+++ b/SSA/Projects/Scf/ScfFunctor.lean
@@ -537,7 +537,7 @@ open ScfRegion in
 theorem correct :
     Com.denote (lhs rgn niters1 niters2 start1) Γv = Com.denote (rhs rgn niters1 niters2 start1) Γv := by
   simp [lhs, rhs, for_, axpy, cst]
-  try simp_peephole [add, iterate, for_, axpy, cst, cst_nat] at Γv
+  simp_peephole [add, iterate, for_, axpy, cst, cst_nat] at Γv
   intros a
   have swap_niters := add_comm (a := niters1) (b := niters2)
   set arg := ((LoopBody.CounterDecorator 1 fun i v =>