cleanup: remove ReadKindFinals from modes.rs output (#2774)

Author: tjhance

source/rust_verify/src/verifier.rs

@@ -2856,7 +2856,7 @@ impl Verifier {
 
         let vir_crate =
             vir::autospec::resolve_autospec(&vir_crate).map_err(|e| (vec![e], Vec::new()))?;
-        let (vir_crate, erasure_modes, _read_kind_finals) =
+        let (vir_crate, erasure_modes) =
             vir::modes::check_crate(&vir_crate).map_err(|es| (es, Vec::new()))?;
 
         self.vir_crate = Some(vir_crate.clone());

source/vir/src/modes.rs

@@ -3974,7 +3974,7 @@ fn check_function(
     Ok(())
 }
 
-pub fn check_crate(krate: &Krate) -> Result<(Krate, ErasureModes, ReadKindFinals), Vec<VirErr>> {
+pub fn check_crate(krate: &Krate) -> Result<(Krate, ErasureModes), Vec<VirErr>> {
     let mut funs: HashMap<Fun, Function> = HashMap::new();
     let mut datatypes: HashMap<Path, Datatype> = HashMap::new();
     for function in krate.functions.iter() {
@@ -4034,9 +4034,5 @@ pub fn check_crate(krate: &Krate) -> Result<(Krate, ErasureModes, ReadKindFinals
             errors.push(err);
         }
     }
-    if errors.len() > 0 {
-        Err(errors)
-    } else {
-        Ok((Arc::new(kratex), record.erasure_modes, record.read_kind_finals))
-    }
+    if errors.len() > 0 { Err(errors) } else { Ok((Arc::new(kratex), record.erasure_modes)) }
 }