diff options
| -rw-r--r-- | theories/Reals/Rfunctions.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 4724d0e531..5eb34324ed 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -525,9 +525,6 @@ Qed. (*******************************) (*i Due to L.Thery i*) -Ltac case_eq name := - generalize (eq_refl name); pattern name at -1; case name. - Definition powerRZ (x:R) (n:Z) := match n with | Z0 => 1 |