From 809ccdbb150240f9623a77dc2fd35367ec8b059f 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 a39b54f264..b749a4f71c 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -382,7 +382,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}.