From 0d4ca112090ee528086ce1fddeecfe79fdada02d Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 5 Jul 2024 22:40:15 +0900
Subject: [PATCH] rm duplicate

---
 theories/realfun.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/realfun.v b/theories/realfun.v
index 1e491567d..8a5bdd953 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -383,7 +383,6 @@ Qed.
 
 End fun_cvg_realType.
 Arguments nondecreasing_at_right_cvgr {R f a} b.
-Arguments nondecreasing_at_right_cvgr {R f a} b.
 
 Section fun_cvg_ereal.
 Context {R : realType}.