cleaning up rebase

math-comp · Oct 20, 2022 · cdf7849 · cdf7849
1 parent 901f46b
commit cdf7849
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 607 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -116,7 +116,6 @@
   + generalize `lte_addl`, `lte_addr`, `gte_subl`, `gte_subr`,
     `lte_daddl`, `lte_daddr`, `gte_dsubl`, `gte_dsubr`
 - in `topology.v`:
-  + lemma `weak_subspace_open`
   + lemmas `continuous_subspace0`, `continuous_subspace1`
 
 - in `realfun.v`:
@@ -173,8 +172,6 @@
   + lemma `lte_spaddr`, renamed `lte_spaddre`
 
 ### Removed
-- in `realFun.v`:
-  + removed `continuous_subspace_itv`
 
 - in file `classical_sets.v`:
   + lemmas `pred_oappE` and `pred_oapp_set` (moved to `mathcomp_extra.v`)