Address issues from code review

Author: jim-portegies

theories/Libs/Analysis/Series.v

@@ -37,7 +37,6 @@ Waterproof Enable Automation RealsAndIntegers.
 #[export] Hint Resolve Rmult_lt_0_compat : wp_reals.
 #[export] Hint Resolve Rinv_lt_contravar : wp_reals.
 
-Waterproof Disable Filter Errors.
 Open Scope R_scope.
 
 Lemma sigma_split_v2 (a : ℕ → ℝ) (k  l M : ℕ) :

theories/Util/BySince.v

@@ -111,7 +111,7 @@ Ltac2 unseal_lemma (xtr_lemma : constr) : ident :=
   assert $unsealed_statement as $aux_id;
   Control.focus 1 1 (fun () => exact $xtr_lemma);
   aux_id.
-Waterproof Disable Filter Errors.
+
 (** Wrapper for the main functionality of 'By ...'-tactics,
   such that the main fucntionality can be reused in 'Since ...'-tactics.
 

theories/Util/ConvertStrings.v

@@ -19,11 +19,8 @@
 Require Import Ltac2.Ltac2.
 From Stdlib Require Import String.
 From Corelib Require Import Byte.
-
-(* Open Scope byte_scope. *)
-
-
 From Stdlib Require Import List.
+
 Import ListNotations.
 Open Scope list_scope.