Skip to content

Commit 809ccdb

Browse files
affeldt-aistaffeldt-aist
committed
rm duplicate
1 parent 258a315 commit 809ccdb

File tree

1 file changed

+0
-1
lines changed

1 file changed

+0
-1
lines changed

‎theories/realfun.v‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -382,7 +382,6 @@ Qed.
382382

383383
End fun_cvg_realType.
384384
Arguments nondecreasing_at_right_cvgr {R f a} b.
385-
Arguments nondecreasing_at_right_cvgr {R f a} b.
386385

387386
Section fun_cvg_ereal.
388387
Context {R : realType}.

0 commit comments

Comments
 (0)