From a18d899a2c2b9bdd36f4a5a4b70472c12a835a96 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jul 2023 14:34:55 +0200
Subject: Finish a first version of the progress tactic

---
 backends/lean/Base/Diverge/Base.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backends/lean/Base/Diverge')

diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index e22eb914..d2c91ff8 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -14,7 +14,7 @@ TODO:
   Actually, the cases from mathlib seems already quite powerful
   (https://leanprover-community.github.io/mathlib_docs/tactics.html#cases)
   For instance: cases h : e
-  Also: cases_matching
+  Also: **casesm**
 - better split tactic
 - we need conversions to operate on the head of applications.
   Actually, something like this works:
-- 
cgit v1.2.3