From 10a77d17ea06b732106348588bedc6a89766d56f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 11 Dec 2023 11:31:43 +0100
Subject: Reactivate the sanity checks for the progress tactic

---
 backends/lean/Base/Progress/Progress.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'backends/lean/Base/Progress/Progress.lean')

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 93b7d7d5..a6a4e82a 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -245,7 +245,7 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
   -- have the proper shape.
   let fExpr ← do
     let isGoal := true
-    withPSpec false isGoal goalTy fun desc => do
+    withPSpec isGoal goalTy fun desc => do
     let fExpr := desc.fArgsExpr
     trace[Progress] "Expression to match: {fExpr}"
     pure fExpr
@@ -386,8 +386,6 @@ namespace Test
     progress keep _ as ⟨ z, h1 .. ⟩
     simp [*, h1]
 
-  set_option trace.Progress false
-
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
     (hmax : x.val + y.val ≤ Scalar.max ty) :
-- 
cgit v1.2.3