From 9d79b8dab238e4c6aeb297ced2a31c2ed5bdf2d6 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Sun, 16 Feb 2025 18:26:57 +0100 Subject: [PATCH] remove extra checks to prevent change from being breaking --- source/rust_verify/src/rust_to_vir_func.rs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs index f32ec0252a..a667aa4a54 100644 --- 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"); }