From eeca1a3d7e316d23ae68cdbd7fcef445262e5861 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 10 Nov 2023 11:10:14 +0100
Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/18224

---
 theories/topology.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/topology.v b/theories/topology.v
index 2ff47d145..85f22c569 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -970,9 +970,9 @@ Tactic Notation "near:" ident(x) :=
   else fail "the goal depends on variables introduced after" x.
 
 Ltac under_near i tac := near=> i; tac; near: i.
-Tactic Notation "near=>" ident(i) "do" tactic1(tac) := under_near i ltac:(tac).
+Tactic Notation "near=>" ident(i) "do" tactic3(tac) := under_near i ltac:(tac).
 Tactic Notation "near=>" ident(i) "do" "[" tactic4(tac) "]" := near=> i do tac.
-Tactic Notation "near" "do" tactic1(tac) :=
+Tactic Notation "near" "do" tactic3(tac) :=
   let i := fresh "i" in under_near i ltac:(tac).
 Tactic Notation "near" "do" "[" tactic4(tac) "]" := near do tac.