diff options
| -rw-r--r-- | theories/Reals/Rcomplete.v (renamed from theories/Reals/Rcomplet.v) | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/theories/Reals/Rcomplet.v b/theories/Reals/Rcomplete.v index 80516e3075..80516e3075 100644 --- a/theories/Reals/Rcomplet.v +++ b/theories/Reals/Rcomplete.v |