diff options
Diffstat (limited to 'theories/Reals/Rtrigo.v')
| -rw-r--r-- | theories/Reals/Rtrigo.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index f9cbb6e9d..c9704db3b 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -22,4 +22,4 @@ Require Import Rsqrt_def. Require Import PSeries_reg. Require Export Rtrigo1. Require Export Ratan. -Require Export Machin.
\ No newline at end of file +Require Export Machin. |