diff --git a/src/passes/08-typer-old/typer.ml b/src/passes/08-typer-old/typer.ml
index c86afc037..43c2e8091 100644
--- a/src/passes/08-typer-old/typer.ml
+++ b/src/passes/08-typer-old/typer.ml
@@ -938,8 +938,8 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
     return (E_let_in {let_binder; rhs; let_result; inline}) let_result.type_expression
   | E_raw_code {language;code;type_anno} ->
     let%bind type_anno = evaluate_type e type_anno in
-    let%bind (_input_type,output_type) = get_t_function type_anno in
-    return (E_raw_code {language;code;type_anno}) output_type
+    let%bind (_input_type,_output_type) = get_t_function type_anno in
+    return (E_raw_code {language;code;type_anno}) type_anno
   | E_recursive {fun_name; fun_type; lambda} ->
     let%bind fun_type = evaluate_type e fun_type in
     let e' = Environment.add_ez_binder fun_name fun_type e in
diff --git a/src/passes/10-transpiler/transpiler.ml b/src/passes/10-transpiler/transpiler.ml
index 278d8df0a..d335b6914 100644
--- a/src/passes/10-transpiler/transpiler.ml
+++ b/src/passes/10-transpiler/transpiler.ml
@@ -616,13 +616,13 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
           aux expr' tree''
        )
   )
-  | E_raw_code { language; code; _} -> 
+  | E_raw_code { language; code; type_anno} -> 
     let backend = "Michelson" in
     let%bind () = trace_strong (language_backend_mismatch language backend ae.location) @@
     Assert.assert_true (String.equal language backend)
     in
-    let code = String.sub code 2 (String.length code - 4) in
-    return @@ E_raw_michelson code
+    let%bind type_anno' = transpile_type type_anno in
+    return @@ E_raw_michelson (code, type_anno')
 
 and transpile_lambda l (input_type , output_type) =
   let { binder ; result } : AST.lambda = l in
diff --git a/src/passes/12-compiler/compiler_program.ml b/src/passes/12-compiler/compiler_program.ml
index 90042c7b3..b3630bccb 100644
--- a/src/passes/12-compiler/compiler_program.ml
+++ b/src/passes/12-compiler/compiler_program.ml
@@ -483,7 +483,12 @@ and translate_expression (expr:expression) (env:environment) : michelson result
         i_push_unit ;
       ]
     )
-  | E_raw_michelson code -> return @@ Michelson.string code
+  | E_raw_michelson (code, type_anno) -> 
+      let (code, _e) = Michelson_parser.V1.parse_expression ~check:false code in
+      let code = Tezos_micheline.Micheline.root code.expanded in
+      let annot = Format.asprintf "(%a)" Mini_c.PP.type_value type_anno in
+
+  return @@ Michelson.prim ~children:[code] ~annot:[annot] I_PUSH
 
 and translate_function_body ({body ; binder} : anon_function) lst input : michelson result =
   let pre_env = Environment.of_list lst in
diff --git a/src/stages/5-mini_c/PP.ml b/src/stages/5-mini_c/PP.ml
index 54f98371d..e9aa005f9 100644
--- a/src/stages/5-mini_c/PP.ml
+++ b/src/stages/5-mini_c/PP.ml
@@ -47,7 +47,7 @@ and type_constant ppf (tb:type_base) : unit =
     | TB_chain_id  -> "chain_id"
     | TB_void      -> "void"
     in
-  fprintf ppf "(TC %s)" s
+  fprintf ppf "%s" s
 
 let rec value ppf : value -> unit = function
   | D_bool b -> fprintf ppf "%b" b
@@ -70,6 +70,21 @@ let rec value ppf : value -> unit = function
   | D_list lst -> fprintf ppf "List[%a]" (list_sep_d value) lst
   | D_set lst -> fprintf ppf "Set[%a]" (list_sep_d value) lst
 
+and type_value_annotated ppf : type_value annotated -> unit = fun (_, tv) ->
+  type_value ppf tv
+
+and type_value ppf : type_value -> unit = function
+  | T_pair (a,b) -> fprintf ppf "pair %a %a" type_value_annotated a type_value_annotated b
+  | T_or    (a,b) -> fprintf ppf "or %a %a" type_value_annotated a type_value_annotated b
+  | T_function (a, b) -> fprintf ppf "lambda (%a) %a" type_value a type_value b
+  | T_base tc -> fprintf ppf "%a" type_constant tc
+  | T_map (k,v) -> fprintf ppf "Map (%a,%a)" type_value k type_value v
+  | T_big_map (k,v) -> fprintf ppf "BigMap (%a,%a)" type_value k type_value v
+  | T_list e -> fprintf ppf "List (%a)" type_value e
+  | T_set e -> fprintf ppf "Set (%a)" type_value e
+  | T_contract c -> fprintf ppf "Contract (%a)" type_value c
+  | T_option c -> fprintf ppf "Option (%a)" type_value c 
+
 and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
   fprintf ppf "%a -> %a" value a value b
 
@@ -110,8 +125,8 @@ and expression_content ppf (e:expression_content) = match e with
       fprintf ppf "@[{ %a@;<1 2>with@;<1 2>{ %a = %a } }@]" expression r (list_sep lr (const ".")) path expression update
   | E_while (e , b) ->
       fprintf ppf "@[while %a do %a@]" expression e expression b
-  | E_raw_michelson code -> 
-      fprintf ppf "{%s}" code 
+  | E_raw_michelson (code, _) -> 
+      fprintf ppf "%s" code 
 
 and expression_with_type : _ -> expression -> _  = fun ppf e ->
   fprintf ppf "%a : %a"
diff --git a/src/stages/5-mini_c/PP.mli b/src/stages/5-mini_c/PP.mli
index 43db6fb4c..d4510b271 100644
--- a/src/stages/5-mini_c/PP.mli
+++ b/src/stages/5-mini_c/PP.mli
@@ -12,6 +12,7 @@ val type_variable : formatter -> type_expression -> unit
 val environment_element : formatter -> environment_element -> unit
 val environment : formatter -> environment -> unit
 val value : formatter -> value -> unit
+val type_value : formatter -> type_value -> unit
 
 (*
 val value_assoc : formatter -> (value * value) -> unit
diff --git a/src/stages/5-mini_c/types.ml b/src/stages/5-mini_c/types.ml
index 81c2186b4..a3a5b22bf 100644
--- a/src/stages/5-mini_c/types.ml
+++ b/src/stages/5-mini_c/types.ml
@@ -91,7 +91,7 @@ and expression_content =
   | E_sequence of (expression * expression)
   | E_record_update of (expression * [`Left | `Right] list * expression)
   | E_while of (expression * expression)
-  | E_raw_michelson of string
+  | E_raw_michelson of (string * type_value)
 
 and expression = {
   content : expression_content ;
diff --git a/src/test/contracts/michelson_insertion.mligo b/src/test/contracts/michelson_insertion.mligo
index 4ab073888..17ee7a64f 100644
--- a/src/test/contracts/michelson_insertion.mligo
+++ b/src/test/contracts/michelson_insertion.mligo
@@ -1,4 +1,5 @@
 // Test michelson insertion in CameLIGO
 
 let michelson_add (n : nat) : nat =
-  [%Michelson {| DUP;ADD; PUSH "hello" |} : nat -> nat ]
+  let f : nat -> nat = [%Michelson {| DUP;ADD |}] in
+  f n
diff --git a/src/test/contracts/michelson_insertion.religo b/src/test/contracts/michelson_insertion.religo
index b397e1934..138b58a6d 100644
--- a/src/test/contracts/michelson_insertion.religo
+++ b/src/test/contracts/michelson_insertion.religo
@@ -1,4 +1,4 @@
 // Test michelson insertion in ReasonLIGO
 
 let michelson_add = (n : nat) : nat =>
-  [%Michelson {| DUP;ADD; PUSH "hello" |} : nat => nat ]
+  [%Michelson {| DUP;ADD |} : nat => nat ]