From 3f229d54374cc57d92d5243dcfa87fd4d2cd8491 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 21 Sep 2022 17:27:27 -0400
Subject: [PATCH] fix: add colGt

---
 src/Init/Conv.lean    | 4 ++--
 src/Init/Tactics.lean | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 68947ad8f9..a25df03ae8 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -82,7 +82,7 @@ syntax (name := change) "change " term : conv
 Like the `delta` tactic, this ignores any definitional equations and uses
 primitive delta-reduction instead, which may result in leaking implementation details.
 Users should prefer `unfold` for unfolding definitions. -/
-syntax (name := delta) "delta " ident+ : conv
+syntax (name := delta) "delta " (colGt ident)+ : conv
 
 /--
 * `unfold foo` unfolds all occurrences of `foo` in the target.
@@ -90,7 +90,7 @@ syntax (name := delta) "delta " ident+ : conv
 Like the `unfold` tactic, this uses equational lemmas for the chosen definition
 to rewrite the target. For recursive definitions,
 only one layer of unfolding is performed. -/
-syntax (name := unfold) "unfold " ident+ : conv
+syntax (name := unfold) "unfold " (colGt ident)+ : conv
 
 /-- `pattern pat` traverses to the first subterm of the target that matches `pat`. -/
 syntax (name := pattern) "pattern " term : conv
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 9f4ea079d4..6b21f9926f 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -462,7 +462,7 @@ syntax (name := dsimp) "dsimp " (config)? (discharger)? (&"only ")?
 This is a low-level tactic, it will expose how recursive definitions have been
 compiled by Lean.
 -/
-syntax (name := delta) "delta " ident+ (location)? : tactic
+syntax (name := delta) "delta " (colGt ident)+ (location)? : tactic
 
 /--
 * `unfold id` unfolds definition `id`.
@@ -472,7 +472,7 @@ For non-recursive definitions, this tactic is identical to `delta`.
 For definitions by pattern matching, it uses "equation lemmas" which are
 autogenerated for each match arm.
 -/
-syntax (name := unfold) "unfold " ident+ (location)? : tactic
+syntax (name := unfold) "unfold " (colGt ident)+ (location)? : tactic
 
 /--
 Auxiliary macro for lifting have/suffices/let/...