remove extra checks to prevent change from being breaking

verus-lang · Feb 16, 2025 · 9d79b8d · 9d79b8d
1 parent dae513a
commit 9d79b8d
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs
@@ -1942,12 +1942,6 @@ fn get_body_visibility_and_fuel(
         // These don't matter for non-spec functions
         Ok((private_vis, FuelOpaqueness::Opaque))
     } else if !has_body {
-        if publish == Some(true) {
-            return err_span(span, "function is marked `open` but it has no body");
-        }
-        if publish == Some(false) {
-            return err_span(span, "function is marked `closed` but it has no body");
-        }
         if opaque || opaque_outside_module {
             return err_span(span, "opaque has no effect on a function without a body");
         }