From 7668037a8daaef7bc8f1fc3225c2e6cc26cac0aa Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 23 May 2017 10:40:51 +0200 Subject: Remove deprecated options from the standard library. --- theories/Reals/SeqProp.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Reals') diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 3697999f7..6a5233b64 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -150,7 +150,7 @@ Definition sequence_lb (Un:nat -> R) (pr:has_lb Un) (* Compatibility *) Notation sequence_majorant := sequence_ub (only parsing). Notation sequence_minorant := sequence_lb (only parsing). -Unset Standard Proposition Elimination Names. + Lemma Wn_decreasing : forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr). Proof. -- cgit v1.2.3