Revert "feat: port Mathlib.Data.Real.CauSeqCompletion (#1440)" (#1468)

This reverts commit 0a713e2. The motivation is to allow leanprover-community/mathlib#18122 to generate pre-port mathport output in the mathlib3port CI. Once that is done, I will unrevert this and merge in the changes it suggests.
leanprover-community · Jan 23, 2023 · 72c7dff · 72c7dff
1 parent f00b352
commit 72c7dff
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 464 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -331,7 +331,6 @@ import Mathlib.Data.Rat.Lemmas
 import Mathlib.Data.Rat.Order
 import Mathlib.Data.Rat.Sqrt
 import Mathlib.Data.Real.CauSeq
-import Mathlib.Data.Real.CauSeqCompletion
 import Mathlib.Data.Rel
 import Mathlib.Data.Semiquot
 import Mathlib.Data.Seq.Computation