diff --git a/Cargo.lock b/Cargo.lock
index c06048ac0..74371ee9d 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -541,7 +541,6 @@ version = "0.2.0"
 dependencies = [
  "hax-lib",
  "hax-lib-macros-types",
- "paste",
  "proc-macro-error2",
  "proc-macro2",
  "quote",
diff --git a/hax-lib/macros/Cargo.toml b/hax-lib/macros/Cargo.toml
index 53538dda4..885144866 100644
--- a/hax-lib/macros/Cargo.toml
+++ b/hax-lib/macros/Cargo.toml
@@ -15,7 +15,6 @@ proc-macro = true
 [target.'cfg(hax)'.dependencies]
 proc-macro-error2 = { version = "2.0" }
 hax-lib-macros-types = { workspace = true }
-paste = { version = "1.0.15" }
 syn = { version = "2.0", features = ["full", "visit-mut", "visit"] }
 
 [dependencies]
diff --git a/hax-lib/macros/src/implementation.rs b/hax-lib/macros/src/implementation.rs
index 117481dfe..7eec0184b 100644
--- a/hax-lib/macros/src/implementation.rs
+++ b/hax-lib/macros/src/implementation.rs
@@ -782,110 +782,108 @@ macro_rules! make_quoting_item_proc_macro {
 
 macro_rules! make_quoting_proc_macro {
     ($backend:ident) => {
-        paste::paste! {
-            #[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")]
-            ///
-
-            /// While it is possible to directly write raw backend code,
-            /// sometimes it can be inconvenient. For example, referencing
-            /// Rust names can be a bit cumbersome: for example, the name
-            /// `my_crate::my_module::CONSTANT` might be translated
-            /// differently in a backend (e.g. in the F* backend, it will
-            /// probably be `My_crate.My_module.v_CONSTANT`).
-            ///
-
-            /// To facilitate this, you can write Rust names directly,
-            /// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3`
-            /// will be replaced with `f My_crate.My_module.v_CONSTANT + 3`
-            /// in the F* backend for instance.
-
-            /// If you want to refer to the Rust constructor
-            /// `Enum::Variant`, you should write `$$Enum::Variant` (note
-            /// the double dollar).
-
-            /// If the name refers to something polymorphic, you need to
-            /// signal it by adding _any_ type informations,
-            /// e.g. `${my_module::function<()>}`. The curly braces are
-            /// needed for such more complex expressions.
-
-            /// You can also write Rust patterns with the `$?{SYNTAX}`
-            /// syntax, where `SYNTAX` is a Rust pattern. The syntax
-            /// `${EXPR}` also allows any Rust expressions
-            /// `EXPR` to be embedded.
-
-            /// Types can be refered to with the syntax `$:{TYPE}`.
-            #[proc_macro]
-            pub fn [<$backend _expr>](payload: pm::TokenStream) -> pm::TokenStream {
-                let ts: TokenStream = quote::expression(quote::InlineExprType::Unit, payload).into();
-                quote!{{
-                    #[cfg([< hax_backend_ $backend >])]
-                    {
-                        #ts
-                    }
-                }}.into()
-            }
+        #[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")]
+        ///
 
-            #[doc = concat!("The `Prop` version of `", stringify!($backend), "_expr`.")]
-            #[proc_macro]
-            pub fn [<$backend _prop_expr>](payload: pm::TokenStream) -> pm::TokenStream {
-                let ts: TokenStream = quote::expression(quote::InlineExprType::Prop, payload).into();
-                quote!{{
-                    #[cfg([< hax_backend_ $backend >])]
-                    {
-                        #ts
-                    }
-                    #[cfg(not([< hax_backend_ $backend >]))]
-                    {
-                        ::hax_lib::Prop::from_bool(true)
-                    }
-                }}.into()
-            }
+        /// While it is possible to directly write raw backend code,
+        /// sometimes it can be inconvenient. For example, referencing
+        /// Rust names can be a bit cumbersome: for example, the name
+        /// `my_crate::my_module::CONSTANT` might be translated
+        /// differently in a backend (e.g. in the F* backend, it will
+        /// probably be `My_crate.My_module.v_CONSTANT`).
+        ///
 
-            #[doc = concat!("The unsafe (because polymorphic: even computationally relevant code can be inlined!) version of `", stringify!($backend), "_expr`.")]
-            #[proc_macro]
-            #[doc(hidden)]
-            pub fn [<$backend _unsafe_expr>](payload: pm::TokenStream) -> pm::TokenStream {
-                let ts: TokenStream = quote::expression(quote::InlineExprType::Anything, payload).into();
-                quote!{{
-                    #[cfg([< hax_backend_ $backend >])]
-                    {
-                        #ts
-                    }
-                }}.into()
-            }
+        /// To facilitate this, you can write Rust names directly,
+        /// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3`
+        /// will be replaced with `f My_crate.My_module.v_CONSTANT + 3`
+        /// in the F* backend for instance.
+
+        /// If you want to refer to the Rust constructor
+        /// `Enum::Variant`, you should write `$$Enum::Variant` (note
+        /// the double dollar).
+
+        /// If the name refers to something polymorphic, you need to
+        /// signal it by adding _any_ type informations,
+        /// e.g. `${my_module::function<()>}`. The curly braces are
+        /// needed for such more complex expressions.
+
+        /// You can also write Rust patterns with the `$?{SYNTAX}`
+        /// syntax, where `SYNTAX` is a Rust pattern. The syntax
+        /// `${EXPR}` also allows any Rust expressions
+        /// `EXPR` to be embedded.
+
+        /// Types can be refered to with the syntax `$:{TYPE}`.
+        #[proc_macro]
+        pub fn ${concat($backend, _expr)}(payload: pm::TokenStream) -> pm::TokenStream {
+            let ts: TokenStream = quote::expression(quote::InlineExprType::Unit, payload).into();
+            quote!{{
+                #[cfg(${concat(hax_backend_, $backend)})]
+                {
+                    #ts
+                }
+            }}.into()
+        }
 
-            make_quoting_item_proc_macro!($backend, [< $backend _before >], ItemQuotePosition::Before, [< hax_backend_ $backend >]);
-            make_quoting_item_proc_macro!($backend, [< $backend _after >], ItemQuotePosition::After, [< hax_backend_ $backend >]);
+        #[doc = concat!("The `Prop` version of `", stringify!($backend), "_expr`.")]
+        #[proc_macro]
+        pub fn ${concat($backend, _prop_expr)}(payload: pm::TokenStream) -> pm::TokenStream {
+            let ts: TokenStream = quote::expression(quote::InlineExprType::Prop, payload).into();
+            quote!{{
+                #[cfg(${concat(hax_backend_, $backend)})]
+                {
+                    #ts
+                }
+                #[cfg(not(${concat(hax_backend_, $backend)}))]
+                {
+                    ::hax_lib::Prop::from_bool(true)
+                }
+            }}.into()
+        }
 
-            #[doc = concat!("Replaces a Rust item with some verbatim ", stringify!($backend)," code.")]
-            #[proc_macro_error]
-            #[proc_macro_attribute]
-            pub fn [< $backend _replace >](payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
-                let item: TokenStream = item.into();
-                let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
-                [< $backend _before >](payload, quote!{#attr #item}.into())
-            }
+        #[doc = concat!("The unsafe (because polymorphic: even computationally relevant code can be inlined!) version of `", stringify!($backend), "_expr`.")]
+        #[proc_macro]
+        #[doc(hidden)]
+        pub fn ${concat($backend, _unsafe_expr)}(payload: pm::TokenStream) -> pm::TokenStream {
+            let ts: TokenStream = quote::expression(quote::InlineExprType::Anything, payload).into();
+            quote!{{
+                #[cfg(${concat(hax_backend_, $backend)})]
+                {
+                    #ts
+                }
+            }}.into()
+        }
 
-            #[doc = concat!("Replaces the body of a Rust function with some verbatim ", stringify!($backend)," code.")]
-            #[proc_macro_error]
-            #[proc_macro_attribute]
-            pub fn [< $backend _replace_body >](payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
-                let payload: TokenStream = payload.into();
-                let item: ItemFn = parse_macro_input!(item);
-                let mut hax_item = item.clone();
-                *hax_item.block.as_mut() = parse_quote!{
-                    {
-                        ::hax_lib::$backend::unsafe_expr!(#payload)
-                    }
-                };
-                quote!{
-                    #[cfg([< hax_backend_ $backend >])]
-                    #hax_item
-
-                    #[cfg(not([< hax_backend_ $backend >]))]
-                    #item
-                }.into()
-            }
+        make_quoting_item_proc_macro!($backend, ${concat($backend, _before)}, ItemQuotePosition::Before, ${concat(hax_backend_, $backend)});
+        make_quoting_item_proc_macro!($backend, ${concat($backend, _after)}, ItemQuotePosition::After, ${concat(hax_backend_, $backend)});
+
+        #[doc = concat!("Replaces a Rust item with some verbatim ", stringify!($backend)," code.")]
+        #[proc_macro_error]
+        #[proc_macro_attribute]
+        pub fn ${concat($backend, _replace)}(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+            let item: TokenStream = item.into();
+            let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
+            ${concat($backend, _before)}(payload, quote!{#attr #item}.into())
+        }
+
+        #[doc = concat!("Replaces the body of a Rust function with some verbatim ", stringify!($backend)," code.")]
+        #[proc_macro_error]
+        #[proc_macro_attribute]
+        pub fn ${concat($backend, _replace_body)}(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+            let payload: TokenStream = payload.into();
+            let item: ItemFn = parse_macro_input!(item);
+            let mut hax_item = item.clone();
+            *hax_item.block.as_mut() = parse_quote!{
+                {
+                    ::hax_lib::$backend::unsafe_expr!(#payload)
+                }
+            };
+            quote!{
+                #[cfg(${concat(hax_backend_, $backend)})]
+                #hax_item
+
+                #[cfg(not(${concat(hax_backend_, $backend)}))]
+                #item
+            }.into()
         }
     };
     ($($backend:ident)*) => {
diff --git a/hax-lib/macros/src/lib.rs b/hax-lib/macros/src/lib.rs
index ec7b1f1b1..b61b72426 100644
--- a/hax-lib/macros/src/lib.rs
+++ b/hax-lib/macros/src/lib.rs
@@ -1,6 +1,8 @@
 // Proc-macros must "reside in the root of the crate": whence the use
 // of `std::include!` instead of proper module declaration.
 
+#![feature(macro_metavar_expr_concat)]
+
 #[cfg(hax)]
 std::include!("implementation.rs");
 
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index a0508a4b8..0e1797caa 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -355,7 +355,6 @@ name = "hax-lib-macros"
 version = "0.2.0"
 dependencies = [
  "hax-lib-macros-types",
- "paste",
  "proc-macro-error2",
  "proc-macro2",
  "quote",
@@ -675,12 +674,6 @@ version = "6.6.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e2355d85b9a3786f481747ced0e0ff2ba35213a1f9bd406ed906554d7af805a1"
 
-[[package]]
-name = "paste"
-version = "1.0.15"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
-
 [[package]]
 name = "pattern-or"
 version = "0.1.0"