refactor(hax-lib-macros): rename verif_status to verification_status

hacspec · Aug 12, 2024 · 2d3ce54 · 2d3ce54
1 parent d0306f4
commit 2d3ce54
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
@@ -45,7 +45,7 @@ pub fn fstar_options(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenS
 /// `panic_free`.
 #[proc_macro_error]
 #[proc_macro_attribute]
-pub fn fstar_verif_status(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+pub fn fstar_verification_status(attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
     let action = format!("{}", parse_macro_input!(attr as Ident));
     match action.as_str() {
         "lax" => {

diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs
@@ -34,7 +34,7 @@ macro_rules! export_quoting_proc_macros {
 export_quoting_proc_macros!(
     fstar(fstar_expr, fstar_unsafe_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar, {
         pub use hax_lib_macros::fstar_options as options;
-        pub use hax_lib_macros::fstar_verif_status as verif_status;
+        pub use hax_lib_macros::fstar_verification_status as verification_status;
     })
 
     coq(coq_expr, coq_unsafe_expr, coq_before, coq_after, coq_replace, hax_backend_coq)