diff options
Diffstat (limited to 'theories/Reals/Rlogic.v')
| -rw-r--r-- | theories/Reals/Rlogic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index 8aadf8f5dd..e535a55683 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -177,7 +177,7 @@ assert (Z: Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)). split; intros H; simpl; unfold g; - destruct (eq_nat_dec 0 n); try reflexivity. + destruct (eq_nat_dec 0 n) as [t|f]; try reflexivity. elim f; auto with *. elimtype False; omega. destruct IHa as [IHa0 IHa1]. |