From 9b1498aa7fe014ac430467919504d35b0a688934 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 16:13:35 +0200
Subject: Fix a naming issue with progress

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

(limited to 'backends')

diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index dabd25b8..1c509775 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -118,17 +118,17 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) (keep : Option Name) (ids
         match hPost with
         | none => do return (.Error m!"Too many ids provided ({ids}): there is no postcondition to split")
         | some hPost => pure hPost
-      let curPostId := (← hPost.fvarId!.getDecl).userName
-      let rec splitPost (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
+      let rec splitPost (prevId : Name) (hPost : Expr) (ids : List Name) : TacticM ProgressError := do
         match ids with
         | [] => pure .Ok -- Stop
         | nid :: ids => do
           trace[Progress] "Splitting post: {hPost}"
           -- Split
           if ← isConj (← inferType hPost) then
-            splitConjTac hPost (some (nid, curPostId)) (λ _ nhPost => splitPost nhPost ids)
+            splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPost nid nhPost ids)
           else return (.Error m!"Too many ids provided ({nid :: ids}) not enough conjuncts to split in the postcondition")
-      splitPost hPost ids
+      let curPostId := (← hPost.fvarId!.getDecl).userName
+      splitPost curPostId hPost ids
     else return .Ok
   match res with
   | .Error _ => return res -- Can we get there? We're using "return"
-- 
cgit v1.2.3