diff --git a/Cargo.lock b/Cargo.lock
index 9b0986b5a..dbc10e3a8 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -559,6 +559,7 @@ dependencies = [
 name = "hax-lib-macros"
 version = "0.1.0-pre.1"
 dependencies = [
+ "hax-lib",
  "hax-lib-macros-types",
  "proc-macro-error",
  "proc-macro2",
diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs
index 0cfbf01ce..c50fdc8c8 100644
--- a/cli/options/src/lib.rs
+++ b/cli/options/src/lib.rs
@@ -259,10 +259,11 @@ pub struct TranslationOptions {
     /// prefixed by modifiers are processed from left to right,
     /// excluding or including items. Each pattern selects a number of
     /// item. The modifiers are:
-    ///
-    ///  - `+`: includes the selected items with their dependencies,
-    /// transitively (e.g. if function `f` calls `g` which in turn
-    /// calls `h`, then `+k::f` includes `f`, `g` and `h`)
+
+    /// {n}{n} - `+`: includes the selected items with their
+    /// dependencies, transitively (e.g. if function `f` calls `g`
+    /// which in turn calls `h`, then `+k::f` includes `f`, `g` and
+    /// `h`)
 
     /// {n} - `+~`: includes the selected items with their direct
     /// dependencies only (following the previous example, `+~k::f`
@@ -299,15 +300,15 @@ pub struct BackendOptions {
     /// Enable engine debugging: dumps the AST at each phase.
     ///
     /// The value of `<DEBUG_ENGINE>` can be either:
-    ///
-    ///  - `interactive` (or `i`): enables debugging of the engine,
+
+    /// {n}{n} - `interactive` (or `i`): enables debugging of the engine,
     /// and visualize interactively in a webapp how a crate was
     /// transformed by each phase, both in Rust-like syntax and
     /// browsing directly the internal AST. By default, the webapp is
     /// hosted on `http://localhost:8000`, the port can be override by
     /// setting the `HAX_DEBUGGER_PORT` environment variable.
-    ///
-    /// - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
+
+    /// {n} - `<FILE>` or `file:<FILE>`: outputs the different AST as JSON
     /// to `<FILE>`. `<FILE>` can be either [-] or a path.
     #[arg(short, long = "debug-engine")]
     pub debug_engine: Option<DebugEngineMode>,
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 97cae64b3..cb365d4e1 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -573,16 +573,20 @@ struct
              kind = UnsupportedMacro { id = [%show: global_ident] macro };
              span = e.span;
            }
-    | Quote { contents; _ } ->
-        List.map
-          ~f:(function
-            | `Verbatim code -> code
-            | `Expr e -> pexpr e |> term_to_string
-            | `Pat p -> ppat p |> pat_to_string)
-          contents
-        |> String.concat |> F.term_of_string
+    | Quote quote -> pquote e.span quote |> F.term_of_string
     | _ -> .
 
+  (** Prints a `quote` to a string *)
+  and pquote span { contents; _ } =
+    List.map
+      ~f:(function
+        | `Verbatim code -> code
+        | `Expr e -> pexpr e |> term_to_string
+        | `Pat p -> ppat p |> pat_to_string
+        | `Typ p -> pty span p |> term_to_string)
+      contents
+    |> String.concat
+
   and parm { arm = { arm_pat; body } } = (ppat arm_pat, None, pexpr body)
 
   module FStarBinder = struct
@@ -793,7 +797,12 @@ struct
         F.mk_e_app effect (if is_lemma then args else typ :: args)
 
   let rec pitem (e : item) :
-      [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list =
+      [> `Impl of F.AST.decl
+      | `Intf of F.AST.decl
+      | `VerbatimImpl of string
+      | `VerbatimIntf of string
+      | `Comment of string ]
+      list =
     try pitem_unwrapped e
     with Diagnostics.SpanFreeError.Exn error ->
       let error = Diagnostics.SpanFreeError.payload error in
@@ -805,7 +814,12 @@ struct
       ]
 
   and pitem_unwrapped (e : item) :
-      [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list =
+      [> `Impl of F.AST.decl
+      | `Intf of F.AST.decl
+      | `VerbatimImpl of string
+      | `VerbatimIntf of string
+      | `Comment of string ]
+      list =
     match e.v with
     | Alias { name; item } ->
         let pat =
@@ -1248,6 +1262,20 @@ struct
         let tcinst = F.term @@ F.AST.Var FStar_Parser_Const.tcinstance_lid in
         F.decls ~fsti:ctx.interface_mode ~attrs:[ tcinst ]
         @@ F.AST.TopLevelLet (NoLetQualifier, [ (pat, body) ])
+    | Quote quote ->
+        let fstar_opts =
+          Attrs.find_unique_attr e.attrs ~f:(function
+            | ItemQuote q -> Some q.fstar_options
+            | _ -> None)
+          |> Option.value_or_thunk ~default:(fun _ ->
+                 Error.assertion_failure e.span
+                   "Malformed `Quote` item: could not find a ItemQuote payload")
+          |> Option.value ~default:Types.{ intf = true; impl = false }
+        in
+        (if fstar_opts.intf then [ `VerbatimIntf (pquote e.span quote) ]
+        else [])
+        @
+        if fstar_opts.impl then [ `VerbatimImpl (pquote e.span quote) ] else []
     | HaxError details ->
         [
           `Comment
@@ -1261,7 +1289,12 @@ end
 module type S = sig
   val pitem :
     item ->
-    [> `Impl of F.AST.decl | `Intf of F.AST.decl | `Comment of string ] list
+    [> `Impl of F.AST.decl
+    | `Intf of F.AST.decl
+    | `VerbatimImpl of string
+    | `VerbatimIntf of string
+    | `Comment of string ]
+    list
 end
 
 let make (module M : Attrs.WITH_ITEMS) ctx =
@@ -1311,6 +1344,8 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
   |> List.concat_map ~f:(function
        | `Impl i -> [ mk_impl (decl_to_string i) ]
        | `Intf i -> [ mk_intf (decl_to_string i) ]
+       | `VerbatimIntf s -> if interface_mode then [ `Intf s ] else [ `Impl s ]
+       | `VerbatimImpl s -> if interface_mode then [ `Impl s ] else [ `Impl s ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
            if interface_mode then [ `Impl s; `Intf s ] else [ `Impl s ])
diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
index 983990ebc..84eb582e1 100644
--- a/engine/backends/proverif/proverif_backend.ml
+++ b/engine/backends/proverif/proverif_backend.ml
@@ -624,6 +624,7 @@ module Make (Options : OPTS) : MAKE = struct
                 ^^ separate_map hardline
                      (fun variant -> fun_and_reduc name variant)
                      variants
+          | Quote quote -> print#quote quote
           | _ -> empty
 
         method! expr_let : lhs:pat -> rhs:expr -> expr fn =
diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
index 91ae9e95d..8eb3bf3ea 100644
--- a/engine/bin/lib.ml
+++ b/engine/bin/lib.ml
@@ -126,7 +126,15 @@ let run (options : Types.engine_options) : Types.output =
 let main (options : Types.engine_options) =
   Printexc.record_backtrace true;
   let result =
-    try Ok (run options) with e -> Error (e, Printexc.get_raw_backtrace ())
+    try Ok (run options) with
+    | Hax_engine.Diagnostics.SpanFreeError.Exn exn ->
+        Error
+          ( Failure
+              ("Uncatched hax exception (please report, this should not \
+                appear): "
+              ^ [%show: Hax_engine.Diagnostics.SpanFreeError.t] exn),
+            Printexc.get_raw_backtrace () )
+    | e -> Error (e, Printexc.get_raw_backtrace ())
   in
   match result with
   | Ok results ->
diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
index bb03c837f..992f83007 100644
--- a/engine/lib/ast.ml
+++ b/engine/lib/ast.ml
@@ -258,15 +258,18 @@ functor
         }
       | Closure of { params : pat list; body : expr; captures : expr list }
       | EffectAction of { action : F.monadic_action; argument : expr }
-      | Quote of {
-          contents : [ `Verbatim of string | `Expr of expr | `Pat of pat ] list;
-          witness : F.quote;
-        }
+      | Quote of quote
           (** A quotation is an inlined piece of backend code
               interleaved with Rust code *)
 
     and expr = { e : expr'; span : span; typ : ty }
 
+    and quote = {
+      contents :
+        [ `Verbatim of string | `Expr of expr | `Pat of pat | `Typ of ty ] list;
+      witness : F.quote;
+    }
+
     and supported_monads =
       | MException of ty
           (** a exception monad, which we use to handle early returns *)
@@ -388,6 +391,7 @@ functor
           is_external : bool;
           rename : string option;
         }
+      | Quote of quote
       | HaxError of string
       | NotImplementedYet
 
diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml
index 64fc30019..56dc32317 100644
--- a/engine/lib/ast_visitors.ml
+++ b/engine/lib/ast_visitors.ml
@@ -434,17 +434,7 @@ functor
               in
               let argument = self#visit_expr env record_payload.argument in
               EffectAction { action; argument }
-          | Quote { contents; witness } ->
-              let contents =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> `Verbatim code
-                    | `Expr e -> `Expr (self#visit_expr env e)
-                    | `Pat p -> `Pat (self#visit_pat env p))
-                  env contents
-              in
-              let witness = self#visit_feature_quote env witness in
-              Quote { contents; witness }
+          | Quote quote -> Quote (self#visit_quote env quote)
 
         method visit_expr (env : 'env) (this : expr) : expr =
           let e = self#visit_expr' env this.e in
@@ -453,6 +443,20 @@ functor
           let out : expr = { e; span; typ } in
           out
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote) : quote
+            =
+          let contents =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> `Verbatim code
+                | `Expr e -> `Expr (self#visit_expr env e)
+                | `Pat p -> `Pat (self#visit_pat env p)
+                | `Typ t -> `Typ (self#visit_ty env t))
+              env contents
+          in
+          let witness = self#visit_feature_quote env witness in
+          { contents; witness }
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : supported_monads =
           match this with
@@ -678,6 +682,7 @@ functor
                 self#visit_option self#visit_string env record_payload.rename
               in
               Use { path; is_external; rename }
+          | Quote quote -> Quote (self#visit_quote env quote)
           | HaxError x0 ->
               let x0 = self#visit_string env x0 in
               HaxError x0
@@ -1461,22 +1466,9 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (EffectAction { action; argument }, reduce_acc)
-          | Quote { contents; witness } ->
-              let list, reduce_acc =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> (`Verbatim code, self#zero)
-                    | `Expr e ->
-                        let e, acc = self#visit_expr env e in
-                        (`Expr e, acc)
-                    | `Pat p ->
-                        let p, acc = self#visit_pat env p in
-                        (`Pat p, acc))
-                  env contents
-              in
-              let witness, reduce_acc' = self#visit_feature_quote env witness in
-              let reduce_acc = self#plus reduce_acc reduce_acc' in
-              (Quote { contents; witness }, reduce_acc)
+          | Quote quote ->
+              let quote, acc = self#visit_quote env quote in
+              (Quote quote, acc)
 
         method visit_expr (env : 'env) (this : expr) : expr * 'acc =
           let e, reduce_acc = self#visit_expr' env this.e in
@@ -1487,6 +1479,27 @@ functor
           let out : expr = { e; span; typ } in
           (out, reduce_acc)
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote)
+            : quote * 'acc =
+          let list, reduce_acc =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> (`Verbatim code, self#zero)
+                | `Expr e ->
+                    let e, acc = self#visit_expr env e in
+                    (`Expr e, acc)
+                | `Pat p ->
+                    let p, acc = self#visit_pat env p in
+                    (`Pat p, acc)
+                | `Typ t ->
+                    let t, acc = self#visit_ty env t in
+                    (`Typ t, acc))
+              env contents
+          in
+          let witness, reduce_acc' = self#visit_feature_quote env witness in
+          let reduce_acc = self#plus reduce_acc reduce_acc' in
+          ({ contents; witness }, reduce_acc)
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : supported_monads * 'acc =
           match this with
@@ -1817,6 +1830,9 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (Use { path; is_external; rename }, reduce_acc)
+          | Quote quote ->
+              let quote, acc = self#visit_quote env quote in
+              (Quote quote, acc)
           | HaxError x0 ->
               let x0, reduce_acc = self#visit_string env x0 in
               (HaxError x0, reduce_acc)
@@ -2602,18 +2618,7 @@ functor
               let reduce_acc' = self#visit_expr env record_payload.argument in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
-          | Quote { contents; witness } ->
-              let reduce_acc =
-                self#visit_list
-                  (fun env -> function
-                    | `Verbatim code -> self#zero
-                    | `Expr e -> self#visit_expr env e
-                    | `Pat p -> self#visit_pat env p)
-                  env contents
-              in
-              let reduce_acc' = self#visit_feature_quote env witness in
-              let reduce_acc = self#plus reduce_acc reduce_acc' in
-              reduce_acc
+          | Quote quote -> self#visit_quote env quote
 
         method visit_expr (env : 'env) (this : expr) : 'acc =
           let reduce_acc = self#visit_expr' env this.e in
@@ -2623,6 +2628,20 @@ functor
           let reduce_acc = self#plus reduce_acc reduce_acc' in
           reduce_acc
 
+        method visit_quote (env : 'env) ({ contents; witness } : quote) : 'acc =
+          let reduce_acc =
+            self#visit_list
+              (fun env -> function
+                | `Verbatim code -> self#zero
+                | `Expr e -> self#visit_expr env e
+                | `Pat p -> self#visit_pat env p
+                | `Typ t -> self#visit_ty env t)
+              env contents
+          in
+          let reduce_acc' = self#visit_feature_quote env witness in
+          let reduce_acc = self#plus reduce_acc reduce_acc' in
+          reduce_acc
+
         method visit_supported_monads (env : 'env) (this : supported_monads)
             : 'acc =
           match this with
@@ -2918,6 +2937,7 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
+          | Quote quote -> self#visit_quote env quote
           | HaxError x0 ->
               let reduce_acc = self#visit_string env x0 in
               reduce_acc
diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml
index b2be72b80..36964e184 100644
--- a/engine/lib/attr_payloads.ml
+++ b/engine/lib/attr_payloads.ml
@@ -57,6 +57,7 @@ module AssocRole = struct
       | ProcessWrite
       | ProcessInit
       | ProtocolMessages
+      | ItemQuote
     [@@deriving show, yojson, compare, sexp, eq]
   end
 
@@ -73,6 +74,7 @@ module AssocRole = struct
     | Ensures -> Ensures
     | Decreases -> Decreases
     | Refine -> Refine
+    | ItemQuote -> ItemQuote
     | ProcessRead -> ProcessRead
     | ProcessWrite -> ProcessWrite
     | ProcessInit -> ProcessInit
@@ -137,7 +139,7 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
   module type WITH_ITEMS = sig
     val item_uid_map : item UId.Map.t
     val item_of_uid : UId.t -> item
-    val associated_items : attrs -> item AssocRole.Map.t
+    val associated_items_per_roles : attrs -> item list AssocRole.Map.t
     val associated_item : AssocRole.t -> attrs -> item option
 
     val associated_fn :
@@ -146,6 +148,19 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
     val associated_expr :
       ?keep_last_args:int -> AssocRole.t -> attrs -> expr option
 
+    val associated_items : AssocRole.t -> attrs -> item list
+
+    val associated_fns :
+      AssocRole.t -> attrs -> (generics * param list * expr) list
+
+    val associated_exprs :
+      ?keep_last_args:int -> AssocRole.t -> attrs -> expr list
+
+    val expect_fn : item -> generics * param list * expr
+
+    val expect_expr :
+      ?keep_last_args:int -> generics * param list * expr -> expr
+
     val associated_expr_rebinding :
       pat list -> AssocRole.t -> attrs -> expr option
     (** Looks up an expression but takes care of rebinding free variables. *)
@@ -201,43 +216,65 @@ module Make (F : Features.T) (Error : Phase_utils.ERROR) = struct
              @@ "Could not find item with UID "
              ^ [%show: UId.t] uid)
 
-    let associated_items : attrs -> item AssocRole.Map.t =
-      let dup role items =
-        let span = List.map ~f:(fun i -> i.span) items |> Span.union_list in
-        Error.assertion_failure span
-        @@ "Cannot associate multiple "
-        ^ [%show: AssocRole.t] role
-      in
+    let associated_items_per_roles : attrs -> item list AssocRole.Map.t =
       raw_associated_item
       >> List.map ~f:(map_snd item_of_uid)
-      >> map_of_alist (module AssocRole) ~dup
+      >> Map.of_alist_multi (module AssocRole)
+
+    let expect_singleton failure = function
+      | [] -> None
+      | [ v ] -> Some v
+      | _ -> failure ()
+    (* Error.assertion_failure span message *)
+
+    let span_of_attrs =
+      List.map ~f:(fun (i : attr) -> i.span) >> Span.union_list
+
+    let find_or_empty role list = Map.find list role |> Option.value ~default:[]
+
+    let associated_items (role : AssocRole.t) (attrs : attrs) : item list =
+      associated_items_per_roles attrs |> find_or_empty role
 
     let associated_item (role : AssocRole.t) (attrs : attrs) : item option =
-      Map.find (associated_items attrs) role
+      associated_items role attrs
+      |> expect_singleton (fun _ ->
+             let span = span_of_attrs attrs in
+             Error.assertion_failure span
+             @@ "Found more than one "
+             ^ [%show: AssocRole.t] role
+             ^ " for this item. Only one is allowed.")
+
+    let expect_fn = function
+      | { v = Fn { generics; params; body; _ }; _ } -> (generics, params, body)
+      | { span; _ } ->
+          Error.assertion_failure span
+            "this associated item was expected to be a `fn` item"
+
+    let expect_expr ?(keep_last_args = 0) (_generics, params, body) =
+      let n =
+        if keep_last_args < 0 then 0 else List.length params - keep_last_args
+      in
+      let params = List.drop params n |> List.map ~f:(fun p -> p.pat) in
+      match params with
+      | [] -> body
+      | _ -> { body with e = Closure { params; body; captures = [] } }
 
     let associated_fn (role : AssocRole.t) :
         attrs -> (generics * param list * expr) option =
-      associated_item role
-      >> Option.map ~f:(function
-           | { v = Fn { generics; params; body; _ }; _ } ->
-               (generics, params, body)
-           | { span; _ } ->
-               Error.assertion_failure span
-                 "this associated item was expected to be a `fn` item")
+      associated_item role >> Option.map ~f:expect_fn
+
+    let associated_fns (role : AssocRole.t) :
+        attrs -> (generics * param list * expr) list =
+      associated_items role >> List.map ~f:expect_fn
 
     (** Looks up an associated expression, optionally keeping `keep_last_args` last arguments. If keep_last_args is negative, then all arguments are kept. *)
     let associated_expr ?(keep_last_args = 0) (role : AssocRole.t) :
         attrs -> expr option =
-      associated_fn role
-      >> Option.map ~f:(fun (_generics, params, body) ->
-             let n =
-               if keep_last_args < 0 then 0
-               else List.length params - keep_last_args
-             in
-             let params = List.drop params n |> List.map ~f:(fun p -> p.pat) in
-             match params with
-             | [] -> body
-             | _ -> { body with e = Closure { params; body; captures = [] } })
+      associated_fn role >> Option.map ~f:(expect_expr ~keep_last_args)
+
+    let associated_exprs ?(keep_last_args = 0) (role : AssocRole.t) :
+        attrs -> expr list =
+      associated_fns role >> List.map ~f:(expect_expr ~keep_last_args)
 
     let associated_expr_rebinding (params : pat list) (role : AssocRole.t)
         (attrs : attrs) : expr option =
diff --git a/engine/lib/dependencies.ml b/engine/lib/dependencies.ml
index 7c3aa6179..97e8488a6 100644
--- a/engine/lib/dependencies.ml
+++ b/engine/lib/dependencies.ml
@@ -65,7 +65,7 @@ module Make (F : Features.T) = struct
                   v#visit_impl_expr () ie @ v#visit_impl_ident () ii)
                 parent_bounds
         | Alias { name = _; item } -> v#visit_concrete_ident () item
-        | Use _ | HaxError _ | NotImplementedYet ->
+        | Use _ | Quote _ | HaxError _ | NotImplementedYet ->
             Set.empty (module Concrete_ident)
       in
       set |> Set.to_list
diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml
index f42be273e..70c65dde0 100644
--- a/engine/lib/diagnostics.ml
+++ b/engine/lib/diagnostics.ml
@@ -44,6 +44,7 @@ module Phase = struct
     | SimplifyMatchReturn
     | SimplifyHoisting
     | DropNeedlessReturns
+    | TransformHaxLibInline
     | DummyA
     | DummyB
     | DummyC
@@ -143,14 +144,14 @@ let failure ~context ~span kind =
   Core.raise_fatal_error { context; kind; span = Span.to_thir span }
 
 module SpanFreeError : sig
-  type t = private Data of Context.t * kind
+  type t = private Data of Context.t * kind [@@deriving show]
 
   exception Exn of t
 
   val payload : t -> Context.t * kind
   val raise : ?span:T.span list -> Context.t -> kind -> 'a
 end = struct
-  type t = Data of Context.t * kind
+  type t = Data of Context.t * kind [@@deriving show]
 
   exception Exn of t
 
diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml
index ff1f6754e..1193c8e3a 100644
--- a/engine/lib/generic_printer/generic_printer.ml
+++ b/engine/lib/generic_printer/generic_printer.ml
@@ -225,16 +225,19 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
                 |> wrap_parens
             | MacroInvokation _ -> print#assertion_failure "MacroInvokation"
             | EffectAction _ -> print#assertion_failure "EffectAction"
-            | Quote { contents; _ } ->
-                List.map
-                  ~f:(function
-                    | `Verbatim code -> string code
-                    | `Expr e -> print#expr_at Expr_Quote e
-                    | `Pat p -> print#pat_at Expr_Quote p)
-                  contents
-                |> concat
+            | Quote quote -> print#quote quote
             | App _ | Construct _ -> super#expr' ctx e
 
+        method quote { contents; _ } =
+          List.map
+            ~f:(function
+              | `Verbatim code -> string code
+              | `Expr e -> print#expr_at Expr_Quote e
+              | `Pat p -> print#pat_at Expr_Quote p
+              | `Typ p -> print#ty_at Expr_Quote p)
+            contents
+          |> concat
+
         method expr_monadic_let
             : monad:supported_monads * F.monadic_binding ->
               lhs:pat ->
@@ -395,6 +398,7 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
               string "fn" ^^ space ^^ print#concrete_ident name ^^ generics
               ^^ params
               ^^ iblock braces (print#expr_at Item_Fn_body body)
+          | Quote quote -> print#quote quote
           | _ -> string "item not implemented"
 
         method generic_param' : generic_param fn =
diff --git a/engine/lib/generic_printer/generic_printer_base.ml b/engine/lib/generic_printer/generic_printer_base.ml
index 0a1e67629..3c55d9430 100644
--- a/engine/lib/generic_printer/generic_printer_base.ml
+++ b/engine/lib/generic_printer/generic_printer_base.ml
@@ -354,6 +354,7 @@ module Make (F : Features.T) = struct
       method arm : arm fn
       method expr : par_state -> expr fn
       method item : item fn
+      method quote : quote fn
       method items : item list fn
     end
 
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index 4edc4209f..376a1c87a 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -122,8 +122,20 @@ let c_attrs : Thir.attribute list -> attrs = List.map ~f:c_attr
 
 let c_item_attrs (attrs : Thir.item_attributes) : attrs =
   (* TODO: This is a quite coarse approximation, we need to reflect
-     that parent/self structure in our AST. *)
-  c_attrs (attrs.attributes @ attrs.parent_attributes)
+     that parent/self structure in our AST. See
+     https://github.com/hacspec/hax/issues/123. *)
+  let self = c_attrs attrs.attributes in
+  let parent = c_attrs attrs.parent_attributes in
+  let parent =
+    (* Repeating associateditem or uid is harmful *)
+    List.filter
+      ~f:(fun payload ->
+        match Attr_payloads.payloads [ payload ] with
+        | [ ((Uid _ | AssociatedItem _), _) ] -> false
+        | _ -> true)
+      parent
+  in
+  self @ parent
 
 type extended_literal =
   | EL_Lit of literal
diff --git a/engine/lib/phases/phase_drop_references.ml b/engine/lib/phases/phase_drop_references.ml
index 4e4727695..c576d99ee 100644
--- a/engine/lib/phases/phase_drop_references.ml
+++ b/engine/lib/phases/phase_drop_references.ml
@@ -68,7 +68,8 @@ struct
 
     and dexpr' (span : span) (e : A.expr') : B.expr' =
       match (UA.unbox_underef_expr { e; span; typ = UA.never_typ }).e with
-      | [%inline_arms If + Literal + Array + Block + QuestionMark + Quote] ->
+      | [%inline_arms
+          If + Literal + Array + Block + QuestionMark + "dexpr'.Quote"] ->
           auto
       | Construct { constructor; is_record; is_struct; fields; base } ->
           Construct
diff --git a/engine/lib/phases/phase_traits_specs.ml b/engine/lib/phases/phase_traits_specs.ml
index 47187c241..3789ada31 100644
--- a/engine/lib/phases/phase_traits_specs.ml
+++ b/engine/lib/phases/phase_traits_specs.ml
@@ -24,7 +24,7 @@ module Make (F : Features.T) =
 
       let ditems (l : A.item list) : B.item list =
         let (module Attrs) = Attrs.with_items l in
-        let f (item : item) : item =
+        let f' (item : item) : item =
           let v =
             match item.v with
             | Trait { name; generics; items } ->
@@ -122,5 +122,12 @@ module Make (F : Features.T) =
           in
           { item with v }
         in
+        let f item =
+          try f' item
+          with Diagnostics.SpanFreeError.Exn (Data (context, kind)) ->
+            let error = Diagnostics.pretty_print_context_kind context kind in
+            let msg = error in
+            B.make_hax_error_item item.span item.ident msg
+        in
         List.map ~f l
     end)
diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.ml b/engine/lib/phases/phase_transform_hax_lib_inline.ml
index 879c273f3..0d448aa6a 100644
--- a/engine/lib/phases/phase_transform_hax_lib_inline.ml
+++ b/engine/lib/phases/phase_transform_hax_lib_inline.ml
@@ -13,7 +13,7 @@ module%inlined_contents Make (F : Features.T) = struct
   include
     Phase_utils.MakeBase (F) (FB)
       (struct
-        let phase_id = Diagnostics.Phase.CfIntoMonads
+        let phase_id = Diagnostics.Phase.TransformHaxLibInline
       end)
 
   module Implem : ImplemT.T = struct
@@ -22,6 +22,7 @@ module%inlined_contents Make (F : Features.T) = struct
     module UA = Ast_utils.Make (F)
     module UB = Ast_utils.Make (FB)
     module Visitors = Ast_visitors.Make (FB)
+    module Attrs = Attr_payloads.Make (F) (Error)
 
     module S = struct
       module A = FA
@@ -69,6 +70,14 @@ module%inlined_contents Make (F : Features.T) = struct
       UB.Reducers.collect_global_idents#visit_pat () pat |> Set.choose
 
     let rec dexpr' span (expr : A.expr') : B.expr' =
+      quote_of_expr' span expr
+      |> Option.map ~f:(fun quote : B.expr' -> B.Quote quote)
+      |> Option.value_or_thunk ~default:(fun _ ->
+             [%inline_body dexpr'] span expr)
+
+    and quote_of_expr (expr : A.expr) = quote_of_expr' expr.span expr.e
+
+    and quote_of_expr' span (expr : A.expr') =
       match expr with
       | App { f = { e = GlobalVar f; _ }; args = [ payload ]; _ }
         when Global_ident.eq_name Hax_lib__inline f ->
@@ -99,14 +108,30 @@ module%inlined_contents Make (F : Features.T) = struct
                 | Some "_pat" ->
                     let pat = extract_pattern e |> Option.value_exn in
                     `Pat pat
+                | Some "_ty" ->
+                    let typ =
+                      match pat.typ with
+                      | TApp { args = [ GType typ ]; _ } -> typ
+                      | _ ->
+                          Stdio.prerr_endline @@ "-pat->" ^ [%show: B.pat] pat;
+                          Stdio.prerr_endline @@ "-expr->"
+                          ^ [%show: B.expr'] e.e;
+                          Error.assertion_failure span
+                            "Malformed call to 'inline': expected type \
+                             `Option<_>`."
+                    in
+                    `Typ typ
                 | _ -> `Expr e)
           in
           let verbatim = split_str ~on:"SPLIT_QUOTE" str in
           let contents =
             let rec f verbatim
                 (code :
-                  [ `Verbatim of string | `Expr of B.expr | `Pat of B.pat ] list)
-                =
+                  [ `Verbatim of string
+                  | `Expr of B.expr
+                  | `Pat of B.pat
+                  | `Typ of B.ty ]
+                  list) =
               match (verbatim, code) with
               | s :: s', code :: code' -> `Verbatim s :: code :: f s' code'
               | [ s ], [] -> [ `Verbatim s ]
@@ -117,16 +142,64 @@ module%inlined_contents Make (F : Features.T) = struct
                   ^ [%show: string list] verbatim
                   ^ "\ncode="
                   ^ [%show:
-                      [ `Verbatim of string | `Expr of B.expr | `Pat of B.pat ]
+                      [ `Verbatim of string
+                      | `Expr of B.expr
+                      | `Pat of B.pat
+                      | `Typ of B.ty ]
                       list] code
             in
             f verbatim code
           in
-          Quote { contents; witness = Features.On.quote }
-      | [%inline_arms "dexpr'.*"] -> auto
+          Some { contents; witness = Features.On.quote }
+      | _ -> None
       [@@inline_ands bindings_of dexpr - dexpr']
 
-    [%%inline_defs "Item.*"]
+    [%%inline_defs "Item.*" - ditems]
+
+    let ditems items =
+      let (module Attrs) = Attrs.with_items items in
+      let f (item : A.item) =
+        let before, after =
+          let map_fst = List.map ~f:fst in
+          try
+            Attrs.associated_items Attr_payloads.AssocRole.ItemQuote item.attrs
+            |> List.map ~f:(fun assoc_item ->
+                   let e : A.expr =
+                     assoc_item |> Attrs.expect_fn |> Attrs.expect_expr
+                   in
+                   let quote =
+                     UA.Expect.block e |> Option.value ~default:e
+                     |> quote_of_expr
+                     |> Option.value_or_thunk ~default:(fun _ ->
+                            Error.assertion_failure assoc_item.span
+                            @@ "Malformed `Quote` item: `quote_of_expr` \
+                                failed. Expression was:\n"
+                            (* ^ (UA.LiftToFullAst.expr e |> Print_rust.pexpr_str) *)
+                            ^ [%show: A.expr] e)
+                   in
+                   let v : B.item' = Quote quote in
+                   let span = e.span in
+                   let position, attr =
+                     Attrs.find_unique_attr assoc_item.attrs ~f:(function
+                       | ItemQuote q as attr -> Some (q.position, attr)
+                       | _ -> None)
+                     |> Option.value_or_thunk ~default:(fun _ ->
+                            Error.assertion_failure assoc_item.span
+                              "Malformed `Quote` item: could not find a \
+                               ItemQuote payload")
+                   in
+                   let attrs = [ Attr_payloads.to_attr attr assoc_item.span ] in
+                   (B.{ v; span; ident = item.ident; attrs }, position))
+            |> List.partition_tf ~f:(snd >> [%matches? Types.Before])
+            |> map_fst *** map_fst
+          with Diagnostics.SpanFreeError.Exn (Data (context, kind)) ->
+            let error = Diagnostics.pretty_print_context_kind context kind in
+            let msg = error in
+            ([ B.make_hax_error_item item.span item.ident msg ], [])
+        in
+        before @ ditem item @ after
+      in
+      List.concat_map ~f items
   end
 
   include Implem
diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml
index 369a0b005..68ed18b3e 100644
--- a/engine/lib/print_rust.ml
+++ b/engine/lib/print_rust.ml
@@ -215,6 +215,19 @@ module Raw = struct
     | MResult t -> !"MResult<" & pty span t & !">"
     | MOption -> !"MOption"
 
+  and pquote span quote =
+    let ( ! ) = pure span in
+    !"quote!("
+    & List.map
+        ~f:(function
+          | `Verbatim code -> !code
+          | `Expr e -> pexpr e
+          | `Pat p -> ppat p
+          | `Typ t -> pty span t)
+        quote.contents
+      |> concat ~sep:!""
+    & !")"
+
   and pexpr' (e : expr) =
     let ( ! ) = pure e.span in
     match e.e with
@@ -317,7 +330,7 @@ module Raw = struct
     | Closure { params; body; _ } ->
         let params = List.map ~f:ppat params |> concat ~sep:!"," in
         !"(|" & params & !"| {" & pexpr body & !"})"
-    | Quote _ -> !"quotation!(..)"
+    | Quote quote -> pquote e.span quote
   (* | _ -> "todo!()" *)
 
   and plhs (e : lhs) span =
@@ -522,6 +535,7 @@ module Raw = struct
             & !"{"
             & List.map ~f:pimpl_item items |> concat ~sep:!"\n"
             & !"}"
+        | Quote quote -> pquote e.span quote & !";"
         | _ -> raise NotImplemented
       in
       pattrs e.attrs & pi
diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
index c793efdea..e55925237 100644
--- a/engine/lib/subtype.ml
+++ b/engine/lib/subtype.ml
@@ -260,14 +260,16 @@ struct
             body = dexpr body;
             captures = List.map ~f:dexpr captures;
           }
-    | Quote { contents; witness } ->
-        let f = function
-          | `Verbatim code -> `Verbatim code
-          | `Expr e -> `Expr (dexpr e)
-          | `Pat p -> `Pat (dpat p)
-        in
-        Quote
-          { contents = List.map ~f contents; witness = S.quote span witness }
+    | Quote quote -> Quote (dquote span quote)
+
+  and dquote (span : span) ({ contents; witness } : A.quote) : B.quote =
+    let f = function
+      | `Verbatim code -> `Verbatim code
+      | `Expr e -> `Expr (dexpr e)
+      | `Pat p -> `Pat (dpat p)
+      | `Typ p -> `Typ (dty span p)
+    in
+    { contents = List.map ~f contents; witness = S.quote span witness }
 
   and dloop_kind (span : span) (k : A.loop_kind) : B.loop_kind =
     match k with
@@ -469,6 +471,7 @@ struct
             }
       | Alias { name; item } -> B.Alias { name; item }
       | Use { path; is_external; rename } -> B.Use { path; is_external; rename }
+      | Quote quote -> Quote (dquote span quote)
       | HaxError e -> B.HaxError e
       | NotImplementedYet -> B.NotImplementedYet
 
diff --git a/hax-lib-macros/Cargo.toml b/hax-lib-macros/Cargo.toml
index 15ed1c009..06605bd67 100644
--- a/hax-lib-macros/Cargo.toml
+++ b/hax-lib-macros/Cargo.toml
@@ -17,3 +17,6 @@ proc-macro2.workspace = true
 quote.workspace = true
 hax-lib-macros-types.workspace = true
 syn = { version = "2.0", features = ["full", "visit-mut", "extra-traits", "parsing"] }
+
+[dev-dependencies]
+hax-lib = { path = "../hax-lib" }
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index 4e4ad3611..b612d5547 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -398,7 +398,7 @@ pub fn attributes(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStr
                                 let (generics, self_ty) = (&item.generics, &item.self_ty);
                                 let where_clause = &generics.where_clause;
                                 ml.tokens = quote! {#decoration, #generics, #where_clause, #self_ty, #tokens};
-                                ml.path = parse_quote! {::hax_lib_macros::impl_fn_decoration};
+                                ml.path = parse_quote! {::hax_lib::impl_fn_decoration};
                             }
                         }
                     }
@@ -541,8 +541,62 @@ pub fn pv_handwritten(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::Toke
     quote! {#attr #item}.into()
 }
 
+macro_rules! make_quoting_item_proc_macro {
+    ($backend:ident, $macro_name:ident, $position:expr, $cfg_name:ident) => {
+        #[doc = concat!("This macro inlines verbatim ", stringify!($backend)," code before a Rust item.")]
+        ///
+        /// This macro takes a string literal containing backend
+        /// code. Just as backend expression macros, this literal can
+        /// contains dollar-prefixed Rust names.
+        ///
+        /// Note: when targetting F*, you can prepend a first
+        /// comma-separated argument: `interface`, `impl` or
+        /// `both`. This controls where the code will apprear: in the
+        /// `fst` or `fsti` files or both.
+        #[proc_macro_error]
+        #[proc_macro_attribute]
+        pub fn $macro_name(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+            let mut fstar_options = None;
+            let item: TokenStream = item.into();
+            let payload = {
+                let mut tokens = payload.into_iter().peekable();
+                if let Some(pm::TokenTree::Ident(ident)) = tokens.peek() {
+                    let ident_str = format!("{}", ident);
+                    fstar_options = Some(ItemQuoteFStarOpts {
+                        intf: ident_str == "interface" || ident_str == "both",
+                        r#impl: ident_str == "impl" || ident_str == "both",
+                    });
+                    if !matches!(ident_str.as_str(), "impl" | "both" | "interface") {
+                        proc_macro_error::abort!(
+                            ident.span(),
+                            "Expected `impl`, `both` or `interface`"
+                        );
+                    }
+                    // Consume the ident
+                    let _ = tokens.next();
+                    // Expect a comma, fail otherwise
+                    let comma = pm::TokenStream::from_iter(tokens.next().into_iter());
+                    let _: syn::token::Comma = parse_macro_input!(comma);
+                }
+                pm::TokenStream::from_iter(tokens)
+            };
+
+            let ts: TokenStream = quote::item(
+                ItemQuote {
+                    position: $position,
+                    fstar_options,
+                },
+                quote! {#[cfg($cfg_name)]},
+                payload,
+                quote! {#item}.into(),
+            )
+            .into();
+            ts.into()
+        }
+    };
+}
 macro_rules! make_quoting_proc_macro {
-    ($backend:ident($cfg_name:ident)) => {
+    ($backend:ident($expr_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident)) => {
         #[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.")]
         ///
 
@@ -573,9 +627,10 @@ macro_rules! make_quoting_proc_macro {
         /// `${EXPR}` also allows any Rust expressions
         /// `EXPR` to be embedded.
 
+        /// Types can be refered to with the syntax `$:{TYPE}`.
         #[proc_macro]
-        pub fn $backend(payload: pm::TokenStream) -> pm::TokenStream {
-            let ts: TokenStream = quote::quote(payload).into();
+        pub fn $expr_name(payload: pm::TokenStream) -> pm::TokenStream {
+            let ts: TokenStream = quote::expression(payload).into();
             quote!{
                 #[cfg($cfg_name)]
                 {
@@ -583,13 +638,25 @@ macro_rules! make_quoting_proc_macro {
                 }
             }.into()
         }
+
+        make_quoting_item_proc_macro!($backend, $before_name, ItemQuotePosition::Before, $cfg_name);
+        make_quoting_item_proc_macro!($backend, $after_name, ItemQuotePosition::After, $cfg_name);
+
+        #[doc = concat!("Replaces a Rust expression with some verbatim ", stringify!($backend)," code.")]
+        #[proc_macro_error]
+        #[proc_macro_attribute]
+        pub fn $replace_name(payload: pm::TokenStream, item: pm::TokenStream) -> pm::TokenStream {
+            let item: TokenStream = item.into();
+            let attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
+            $before_name(payload, quote!{#attr #item}.into())
+        }
     };
-    ($backend:ident($cfg_name:ident) $($others:tt)+) => {
-        make_quoting_proc_macro!($backend($cfg_name));
+    ($backend:ident $payload:tt $($others:tt)+) => {
+        make_quoting_proc_macro!($backend$payload);
         make_quoting_proc_macro!($($others)+);
     }
 }
 
-make_quoting_proc_macro!(fstar(hax_backend_fstar)
-                         coq(hax_backend_coq)
-                         proverif(hax_backend_proverif));
+make_quoting_proc_macro!(fstar(fstar_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar)
+                         coq(coq_expr, coq_before, coq_after, coq_replace, hax_backend_coq)
+                         proverif(proverif_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif));
diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs
index 7ccf70c9d..b06927817 100644
--- a/hax-lib-macros/src/quote.rs
+++ b/hax-lib-macros/src/quote.rs
@@ -9,7 +9,8 @@
 //! The `<PREFIX>` describes the kind of the antiquotation:
 //!  - empty prefix, the antiquotation is an expression;
 //!  - `?`, the antiquotation is a pattern;
-//!  - `$`, the antiquotation is a constructor name.
+//!  - `$`, the antiquotation is a constructor name;
+//!  - `:`, the antiquotation is a type.
 
 use crate::prelude::*;
 use quote::ToTokens;
@@ -22,6 +23,7 @@ enum AntiquoteKind {
     Expr,
     Constructor,
     Pat,
+    Ty,
 }
 
 impl ToTokens for AntiquoteKind {
@@ -31,6 +33,7 @@ impl ToTokens for AntiquoteKind {
                 Self::Expr => quote! {_expr},
                 Self::Constructor => quote! {_constructor},
                 Self::Pat => quote! {_pat},
+                Self::Ty => quote! {_ty},
             }]
             .into_iter(),
         )
@@ -55,12 +58,13 @@ impl ToTokens for Antiquote {
             AntiquoteKind::Expr => ts,
             AntiquoteKind::Constructor => wrap_pattern(quote! {#ts {..}}),
             AntiquoteKind::Pat => wrap_pattern(ts),
+            AntiquoteKind::Ty => quote! {None::<#ts>},
         };
         tokens.extend([ts].into_iter())
     }
 }
 
-/// Extract antiquotations (`$[?][$]...`, `$[?][$]{...}`) and parses them.
+/// Extract antiquotations (`$[?][$][:]...`, `$[?][$][:]{...}`) and parses them.
 fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), String> {
     let mut chars = s.chars().peekable();
     let mut antiquotations = vec![];
@@ -70,10 +74,11 @@ fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), Stri
             '$' => {
                 let mut s = String::new();
                 let mut kind = AntiquoteKind::Expr;
-                if let Some(prefix) = chars.next_if(|ch| *ch == '?' || *ch == '$') {
+                if let Some(prefix) = chars.next_if(|ch| *ch == '?' || *ch == '$' || *ch == ':') {
                     kind = match prefix {
                         '?' => AntiquoteKind::Pat,
                         '$' => AntiquoteKind::Constructor,
+                        ':' => AntiquoteKind::Ty,
                         _ => unreachable!(),
                     };
                 }
@@ -93,9 +98,9 @@ fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), Stri
                         s.push(ch);
                     }
                 } else {
-                    while let Some(ch) =
-                        chars.next_if(|ch| !matches!(ch, ' ' | '\t' | '\n' | '(' | '{' | ')'))
-                    {
+                    while let Some(ch) = chars.next_if(|ch| {
+                        !matches!(ch, ' ' | '\t' | '\n' | '(' | '{' | ')' | ';' | '!' | '?')
+                    }) {
                         s.push(ch)
                     }
                 }
@@ -124,29 +129,64 @@ fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), Stri
     Ok((output, antiquotations))
 }
 
-pub(super) fn quote(payload: pm::TokenStream) -> pm::TokenStream {
-    let payload = parse_macro_input!(payload as LitStr).value();
-
-    if payload.find(SPLIT_MARK).is_some() {
-        return quote! {std::compile_error!(std::concat!($SPLIT_MARK, " is reserved"))}.into();
+pub(super) fn item(
+    kind: ItemQuote,
+    attribute_to_inject: TokenStream,
+    payload: pm::TokenStream,
+    item: pm::TokenStream,
+) -> pm::TokenStream {
+    let expr = TokenStream::from(expression(payload));
+    let item = TokenStream::from(item);
+    let uid = ItemUid::fresh();
+    let uid_attr = AttrPayload::Uid(uid.clone());
+    let assoc_attr = AttrPayload::AssociatedItem {
+        role: AssociationRole::ItemQuote,
+        item: uid,
+    };
+    let kind_attr = AttrPayload::ItemQuote(kind);
+    let status_attr = AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true });
+    use AttrPayload::NeverDropBody;
+    quote! {
+        #assoc_attr
+        #item
+        #attribute_to_inject
+        #status_attr
+        const _: () = {
+            #NeverDropBody
+            #uid_attr
+            #kind_attr
+            fn quote_contents() {
+                #expr
+            }
+        };
     }
+    .into()
+}
 
-    let (string, antiquotes) = match process_string(&payload) {
-        Ok(x) => x,
-        Err(message) => return quote! {std::compile_error!(#message)}.into(),
+pub(super) fn expression(payload: pm::TokenStream) -> pm::TokenStream {
+    let (mut backend_code, antiquotes) = {
+        let payload = parse_macro_input!(payload as LitStr).value();
+        if payload.find(SPLIT_MARK).is_some() {
+            return quote! {std::compile_error!(std::concat!($SPLIT_MARK, " is reserved"))}.into();
+        }
+        let (string, antiquotes) = match process_string(&payload) {
+            Ok(x) => x,
+            Err(message) => return quote! {std::compile_error!(#message)}.into(),
+        };
+        let string = proc_macro2::Literal::string(&string);
+        let string: TokenStream = [proc_macro2::TokenTree::Literal(string)]
+            .into_iter()
+            .collect();
+        (quote! {#string}, antiquotes)
     };
-    let string = proc_macro2::Literal::string(&string);
-    let string: TokenStream = [proc_macro2::TokenTree::Literal(string)]
-        .into_iter()
-        .collect();
-    let mut code = quote! {#string};
+
     for user in antiquotes.iter().rev() {
         let kind = &user.kind;
-        code = quote! {
+        backend_code = quote! {
             let #kind = #user;
-            #code
+            #backend_code
         };
     }
 
-    quote! {hax_lib::inline(#[allow(unused_variables)]{#code})}.into()
+    quote! {::hax_lib::inline(#[allow(unused_variables)]{#backend_code})}.into()
 }
diff --git a/hax-lib-macros/types/src/lib.rs b/hax-lib-macros/types/src/lib.rs
index aa5fee516..50ada5751 100644
--- a/hax-lib-macros/types/src/lib.rs
+++ b/hax-lib-macros/types/src/lib.rs
@@ -44,6 +44,9 @@ pub enum ItemStatus {
     Excluded { modeled_by: Option<String> },
 }
 
+/// An item can be associated to another one for multiple reasons:
+/// `AssociationRole` capture the nature of the (directed) relation
+/// between two items
 #[derive(Debug, Copy, Clone, Serialize, Deserialize)]
 #[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
 #[serde(rename = "HaAssocRole")]
@@ -52,12 +55,48 @@ pub enum AssociationRole {
     Ensures,
     Decreases,
     Refine,
+    /// A quoted piece of backend code to place after or before the
+    /// extraction of the marked item
+    ItemQuote,
     ProcessRead,
     ProcessWrite,
     ProcessInit,
     ProtocolMessages,
 }
 
+/// Where should a item quote appear?
+#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
+#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
+#[serde(rename = "HaItemQuotePosition")]
+pub enum ItemQuotePosition {
+    /// Should appear just before the item in the extraction
+    Before,
+    /// Should appear right after the item in the extraction
+    After,
+}
+
+/// F*-specific options for item quotes
+#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
+#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
+#[serde(rename = "HaItemQuoteFStarOpts")]
+pub struct ItemQuoteFStarOpts {
+    /// Shall we output this in F* interfaces (`*.fsti` files)?
+    pub intf: bool,
+    /// Shall we output this in F* implementations (`*.fst` files)?
+    pub r#impl: bool,
+}
+
+/// An item quote is a verbatim piece of backend code included in
+/// Rust. [`ItemQuote`] encodes the various options a item quote can
+/// have.
+#[derive(Debug, Copy, Clone, Serialize, Deserialize)]
+#[cfg_attr(feature = "schemars", derive(schemars::JsonSchema))]
+#[serde(rename = "HaItemQuote")]
+pub struct ItemQuote {
+    pub position: ItemQuotePosition,
+    pub fstar_options: Option<ItemQuoteFStarOpts>,
+}
+
 /// Hax only understands one attribute: `#[hax::json(PAYLOAD)]` where
 /// `PAYLOAD` is a JSON serialization of an inhabitant of
 /// `AttrPayload`.
@@ -66,11 +105,16 @@ pub enum AssociationRole {
 #[serde(rename = "HaPayload")]
 pub enum AttrPayload {
     ItemStatus(ItemStatus),
+    /// Mark an item as associated with another one
     AssociatedItem {
+        /// What is the nature of the association?
         role: AssociationRole,
+        /// What is the identifier of the target item?
         item: ItemUid,
     },
     Uid(ItemUid),
+    /// Decides of the position of a item quote
+    ItemQuote(ItemQuote),
     /// Mark an item so that hax never drop its body (this is useful
     /// for pre- and post- conditions of a function we dropped the
     /// body of: pre and post are part of type signature)
diff --git a/hax-lib/Cargo.toml b/hax-lib/Cargo.toml
index 43de0e731..6c3f803ad 100644
--- a/hax-lib/Cargo.toml
+++ b/hax-lib/Cargo.toml
@@ -12,4 +12,8 @@ description = "Hax-specific helpers for Rust programs"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-hax-lib-macros = {path = "../hax-lib-macros"}
+hax-lib-macros = { path = "../hax-lib-macros", optional = true }
+
+[features]
+default = ["macros"]
+macros = ["dep:hax-lib-macros"]
diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs
index a9286c7ed..549a3393e 100644
--- a/hax-lib/src/lib.rs
+++ b/hax-lib/src/lib.rs
@@ -15,6 +15,9 @@
 
 #![no_std]
 
+mod proc_macros;
+pub use proc_macros::*;
+
 #[doc(hidden)]
 #[cfg(hax)]
 #[macro_export]
@@ -130,8 +133,6 @@ pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool {
     !lhs || rhs()
 }
 
-pub use hax_lib_macros::*;
-
 /// Dummy function that carries a string to be printed as such in the output language
 #[doc(hidden)]
 pub fn inline(_: &str) {}
diff --git a/hax-lib/src/proc_macros.rs b/hax-lib/src/proc_macros.rs
new file mode 100644
index 000000000..24570f386
--- /dev/null
+++ b/hax-lib/src/proc_macros.rs
@@ -0,0 +1,32 @@
+//! This module re-exports macros from `hax-lib-macros` since a
+//! proc-macro crate cannot export anything but procedural macros.
+
+pub use hax_lib_macros::{
+    attributes, ensures, exclude, impl_fn_decoration, include, lemma, opaque_type, requires,
+};
+
+pub use hax_lib_macros::{
+    process_init, process_read, process_write, protocol_messages, pv_constructor, pv_handwritten,
+};
+
+macro_rules! export_quoting_proc_macros {
+    ($backend:ident($expr_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident)) => {
+        pub use hax_lib_macros::$expr_name as $backend;
+
+        #[doc=concat!("Procedural macros for ", stringify!($backend))]
+        pub mod $backend {
+            pub use hax_lib_macros::$after_name as after;
+            pub use hax_lib_macros::$before_name as before;
+            pub use hax_lib_macros::$replace_name as replace;
+        }
+    };
+
+    ($backend:ident $payload:tt $($others:tt)+) => {
+        export_quoting_proc_macros!($backend$payload);
+        export_quoting_proc_macros!($($others)+);
+    }
+}
+
+export_quoting_proc_macros!(fstar(fstar_expr, fstar_before, fstar_after, fstar_replace, hax_backend_fstar)
+                         coq(coq_expr, coq_before, coq_after, coq_replace, hax_backend_coq)
+                         proverif(proverif_expr, proverif_before, proverif_after, proverif_replace, hax_backend_proverif));
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index 98d940c6e..bfeaf0a6c 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -26,6 +26,24 @@ exit = 0
 diagnostics = []
 
 [stdout.files]
+"Attributes.Int_model.fst" = '''
+module Attributes.Int_model
+#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
+open Core
+open FStar.Mul
+
+unfold type t_Int = int
+
+unfold let add x y = x + y
+
+unfold instance impl: Core.Ops.Arith.t_Sub t_Int t_Int =
+  {
+    f_Output = t_Int;
+    f_sub_pre = (fun (self: t_Int) (other: t_Int) -> true);
+    f_sub_post = (fun (self: t_Int) (other: t_Int) (out: t_Int) -> true);
+    f_sub = fun (self: t_Int) (other: t_Int) -> self + other
+  }
+'''
 "Attributes.Newtype_pattern.fst" = '''
 module Attributes.Newtype_pattern
 #set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
@@ -133,6 +151,8 @@ let inlined_code__V: u8 = 12uy
 
 let u32_max: u32 = 90000ul
 
+unfold let some_function _ = "hello from F*"
+
 let add3 (x y z: u32)
     : Prims.Pure u32
       (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
@@ -150,6 +170,8 @@ type t_Foo = {
   f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
 }
 
+let before_inlined_code = "example before"
+
 let inlined_code (foo: t_Foo) : Prims.unit =
   let vv_a:i32 = 13l in
   let _:Prims.unit =
@@ -158,4 +180,6 @@ let inlined_code (foo: t_Foo) : Prims.unit =
     add3 ((fun _ -> 3ul) foo) vv_a inlined_code__V y
   in
   ()
+
+let inlined_code_after = "example after"
 '''
diff --git a/tests/Cargo.lock b/tests/Cargo.lock
index aaaf2d857..03661228f 100644
--- a/tests/Cargo.lock
+++ b/tests/Cargo.lock
@@ -40,7 +40,6 @@ name = "attributes"
 version = "0.1.0"
 dependencies = [
  "hax-lib",
- "hax-lib-macros",
  "serde",
 ]
 
diff --git a/tests/attributes/Cargo.toml b/tests/attributes/Cargo.toml
index dfe6b8158..406ede1c7 100644
--- a/tests/attributes/Cargo.toml
+++ b/tests/attributes/Cargo.toml
@@ -4,7 +4,6 @@ version = "0.1.0"
 edition = "2021"
 
 [dependencies]
-hax-lib-macros = { path = "../../hax-lib-macros" }
 hax-lib = { path = "../../hax-lib" }
 serde = { version = "1.0", features = ["derive"] }
 
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index 7c8dfdf4b..cab615b18 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -1,4 +1,4 @@
-use hax_lib_macros as hax;
+use hax_lib as hax;
 
 // dummy max value
 const u32_max: u32 = 90000;
@@ -64,7 +64,7 @@ mod refined_arithmetic {
 }
 
 mod refined_indexes {
-    use hax_lib_macros as hax;
+    use hax_lib as hax;
     const MAX: usize = 10;
     struct MyArray(pub [u8; MAX]);
 
@@ -95,7 +95,7 @@ mod refined_indexes {
     }
 }
 mod newtype_pattern {
-    use hax_lib_macros as hax;
+    use hax_lib as hax;
 
     const MAX: usize = 10;
     #[hax::attributes]
@@ -124,6 +124,8 @@ mod newtype_pattern {
     }
 }
 
+#[hax::fstar::before(r#"let before_${inlined_code} = "example before""#)]
+#[hax::fstar::after(r#"let ${inlined_code}_after = "example after""#)]
 fn inlined_code(foo: Foo) {
     const V: u8 = 12;
     let v_a = 13;
@@ -134,3 +136,41 @@ fn inlined_code(foo: Foo) {
         "
     );
 }
+
+#[hax::fstar::replace(r#"unfold let $some_function _ = "hello from F*""#)]
+fn some_function() -> String {
+    String::from("hello from Rust")
+}
+
+/// An minimal example of a model of math integers for F*
+mod int_model {
+    use super::hax;
+    #[hax::fstar::replace(r#"unfold type $:{Int} = int"#)]
+    #[derive(Copy, Clone)]
+    struct Int(u128);
+
+    #[hax::fstar::replace(r#"unfold let ${add} x y = x + y"#)]
+    fn add(x: Int, y: Int) -> Int {
+        Int(x.0 + y.0)
+    }
+
+    use std::ops::Sub;
+    #[hax::fstar::replace(
+        r#"
+unfold instance impl: Core.Ops.Arith.t_Sub $:Int $:Int =
+  {
+    f_Output = $:Int;
+    f_sub_pre = (fun (self: $:Int) (other: $:Int) -> true);
+    f_sub_post = (fun (self: $:Int) (other: $:Int) (out: $:Int) -> true);
+    f_sub = fun (self: $:Int) (other: $:Int) -> self + other
+  }
+"#
+    )]
+    impl Sub for Int {
+        type Output = Self;
+
+        fn sub(self, other: Self) -> Self::Output {
+            Self(self.0 + other.0)
+        }
+    }
+}