diff --git a/doc/plugin_tutorial/tuto4/src/myexternals.ml b/doc/plugin_tutorial/tuto4/src/myexternals.ml
index 83df4f9a07a2..da6c88235995 100644
--- a/doc/plugin_tutorial/tuto4/src/myexternals.ml
+++ b/doc/plugin_tutorial/tuto4/src/myexternals.ml
@@ -96,12 +96,15 @@ let of_custom = function
    This needs to look at the low-level valexpr data.
    If an external is declared with an incorrect Ltac2 type it may be passed
    invalid values, in which case we assert false. *)
-let to_custom = let open Tac2val in function
-  | ValInt 0 -> A
-  | ValBlk (0, [|c|]) ->
-    (* [to_constr] is [Tac2ffi.to_constr] *)
-    B (to_constr c)
-  | _ -> assert false
+let to_custom v = let open Tac2val in
+  if is_int v then
+    let () = assert (unsafe_to_int v = 0) in
+    A
+  else match unsafe_to_fat v with
+    | ValBlk (0, [|c|]) ->
+      (* [to_constr] is [Tac2ffi.to_constr] *)
+      B (to_constr c)
+    | _ -> assert false
 
 
 (* Now we package both translation functions into a Tac2ffi.repr
diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index 71f0653813b7..8ddc3a5da36f 100644
--- a/plugins/ltac2/tac2core.ml
+++ b/plugins/ltac2/tac2core.ml
@@ -108,13 +108,16 @@ open Core
 let v_blk = Valexpr.make_block
 
 let of_relevance = function
-  | Sorts.Relevant -> ValInt 0
-  | Sorts.Irrelevant -> ValInt 1
-  | Sorts.RelevanceVar q -> ValBlk (0, [|of_qvar q|])
-
-let to_relevance = function
-  | ValInt 0 -> Sorts.Relevant
-  | ValInt 1 -> Sorts.Irrelevant
+  | Sorts.Relevant -> of_int 0
+  | Sorts.Irrelevant -> of_int 1
+  | Sorts.RelevanceVar q -> of_fat @@ ValBlk (0, [|of_qvar q|])
+
+let to_relevance v =
+  if is_int v then match unsafe_to_int v with
+  | 0 -> Sorts.Relevant
+  | 1 -> Sorts.Irrelevant
+  | _ -> assert false
+  else match unsafe_to_fat v with
   | ValBlk (0, [|qvar|]) ->
     let qvar = to_qvar qvar in
     Sorts.RelevanceVar qvar
@@ -136,12 +139,15 @@ let to_rec_declaration (nas, cs) =
   Tac2ffi.to_array Tac2ffi.to_constr cs)
 
 let of_case_invert = let open Constr in function
-  | NoInvert -> ValInt 0
+  | NoInvert -> of_int 0
   | CaseInvert {indices} ->
     v_blk 0 [|of_array of_constr indices|]
 
-let to_case_invert = let open Constr in function
-  | ValInt 0 -> NoInvert
+let to_case_invert v = let open Constr in
+  if is_int v then
+    let () = assert (unsafe_to_int v = 0) in
+    NoInvert
+  else match unsafe_to_fat v with
   | ValBlk (0, [|indices|]) ->
     let indices = to_array to_constr indices in
     CaseInvert {indices}
diff --git a/plugins/ltac2/tac2env.ml b/plugins/ltac2/tac2env.ml
index a89d98e204f0..5366920f55db 100644
--- a/plugins/ltac2/tac2env.ml
+++ b/plugins/ltac2/tac2env.ml
@@ -143,8 +143,8 @@ module MLMap = Map.Make(ML)
 let primitive_map = ref MLMap.empty
 
 let define_primitive name f =
-  let f = match f with
-    | ValCls f -> ValCls (annotate_closure (FrPrim name) f)
+  let f = if is_int f then f else match force_to_fat f with
+    | ValCls f -> of_fat @@ ValCls (annotate_closure (FrPrim name) f)
     | _ -> f
   in
   primitive_map := MLMap.add name f !primitive_map
diff --git a/plugins/ltac2/tac2extffi.ml b/plugins/ltac2/tac2extffi.ml
index 1c663ce1e60d..ff71dc53db45 100644
--- a/plugins/ltac2/tac2extffi.ml
+++ b/plugins/ltac2/tac2extffi.ml
@@ -26,13 +26,16 @@ let to_qhyp v = match Value.to_block v with
 
 let qhyp = make_to_repr to_qhyp
 
-let to_bindings = function
-| ValInt 0 -> NoBindings
-| ValBlk (0, [| vl |]) ->
-  ImplicitBindings (Value.to_list Value.to_constr vl)
-| ValBlk (1, [| vl |]) ->
-  ExplicitBindings ((Value.to_list (fun p -> to_pair to_qhyp Value.to_constr p) vl))
-| _ -> assert false
+let to_bindings v =
+  if is_int v then
+    let () = assert (unsafe_to_int v = 0) in
+    NoBindings
+  else match unsafe_to_fat v with
+    | ValBlk (0, [| vl |]) ->
+      ImplicitBindings (Value.to_list Value.to_constr vl)
+    | ValBlk (1, [| vl |]) ->
+      ExplicitBindings ((Value.to_list (fun p -> to_pair to_qhyp Value.to_constr p) vl))
+    | _ -> assert false
 
 let bindings = make_to_repr to_bindings
 
diff --git a/plugins/ltac2/tac2ffi.ml b/plugins/ltac2/tac2ffi.ml
index 71d20dbe5bba..c54b7df6a661 100644
--- a/plugins/ltac2/tac2ffi.ml
+++ b/plugins/ltac2/tac2ffi.ml
@@ -78,32 +78,28 @@ let valexpr = {
   r_to = (fun obj -> obj);
 }
 
-let of_unit () = ValInt 0
+let of_unit () = of_int 0
 
-let to_unit = function
-| ValInt 0 -> ()
-| _ -> assert false
+let to_unit v = assert (force_to_int v = 0)
 
 let unit = {
   r_of = of_unit;
   r_to = to_unit;
 }
 
-let of_int n = ValInt n
-let to_int = function
-| ValInt n -> n
-| _ -> assert false
+let of_int = of_int
+let to_int = force_to_int
 
 let int = {
   r_of = of_int;
   r_to = to_int;
 }
 
-let of_bool b = if b then ValInt 0 else ValInt 1
+let of_bool b = if b then of_int 0 else of_int 1
 
-let to_bool = function
-| ValInt 0 -> true
-| ValInt 1 -> false
+let to_bool v = match force_to_int v with
+| 0 -> true
+| 1 -> false
 | _ -> assert false
 
 let bool = {
@@ -111,18 +107,16 @@ let bool = {
   r_to = to_bool;
 }
 
-let of_char n = ValInt (Char.code n)
-let to_char = function
-| ValInt n -> Char.chr n
-| _ -> assert false
+let of_char n = of_int (Char.code n)
+let to_char v = Char.chr @@ force_to_int v
 
 let char = {
   r_of = of_char;
   r_to = to_char;
 }
 
-let of_bytes s = ValStr s
-let to_bytes = function
+let of_bytes s = of_fat @@ ValStr s
+let to_bytes v = match force_to_fat v with
 | ValStr s -> s
 | _ -> assert false
 
@@ -139,20 +133,23 @@ let string = {
 }
 
 let rec of_list f = function
-| [] -> ValInt 0
-| x :: l -> ValBlk (0, [| f x; of_list f l |])
+| [] -> of_int 0
+| x :: l -> of_fat @@ ValBlk (0, [| f x; of_list f l |])
 
-let rec to_list f = function
-| ValInt 0 -> []
-| ValBlk (0, [|v; vl|]) -> f v :: to_list f vl
-| _ -> assert false
+let rec to_list f v =
+  if is_int v then
+    let () = assert (unsafe_to_int v = 0) in
+    []
+  else match unsafe_to_fat v with
+    | ValBlk (0, [|v; vl|]) -> f v :: to_list f vl
+    | _ -> assert false
 
 let list r = {
   r_of = (fun l -> of_list r.r_of l);
   r_to = (fun l -> to_list r.r_to l);
 }
 
-let of_closure cls = ValCls cls
+let of_closure cls = of_fat @@ ValCls cls
 
 let to_closure = Tac2val.to_closure
 
@@ -196,9 +193,9 @@ let fun2 arg1 arg2 res = {
 }
 
 let of_ext tag c =
-  ValExt (tag, c)
+  of_fat @@ ValExt (tag, c)
 
-let to_ext tag = function
+let to_ext tag v = match force_to_fat v with
 | ValExt (tag', e) -> extract_val tag tag' e
 | _ -> assert false
 
@@ -247,6 +244,8 @@ let of_rewstrategy ev = of_ext val_rewstrategy ev
 let to_rewstrategy ev = to_ext val_rewstrategy ev
 let rewstrategy = repr_ext val_rewstrategy
 
+let rocq_core n = Names.(KerName.make Tac2env.rocq_prefix (Label.of_id @@ Id.of_string_soft n))
+
 let internal_err =
   let open Names in
   let rocq_prefix =
@@ -269,10 +268,10 @@ let err = repr_ext val_exn
 
 (** FIXME: handle backtrace in Ltac2 exceptions *)
 let of_exn c = match fst c with
-| LtacError (kn, c) -> ValOpn (kn, c)
-| _ -> ValOpn (internal_err, [|of_err c|])
+| LtacError (kn, c) -> of_fat @@ ValOpn (kn, c)
+| _ -> of_fat @@ ValOpn (internal_err, [|of_err c|])
 
-let to_exn c = match c with
+let to_exn c = match force_to_fat c with
 | ValOpn (kn, c) ->
   if Names.KerName.equal kn internal_err then
     to_err c.(0)
@@ -286,10 +285,10 @@ let exn = {
 }
 
 let of_result of_ok = function
-  | Ok v -> ValBlk (0, [|of_ok v|])
-  | Error e -> ValBlk (1, [|of_exn e|])
+  | Ok v -> of_fat @@ ValBlk (0, [|of_ok v|])
+  | Error e -> of_fat @@ ValBlk (1, [|of_exn e|])
 
-let to_result to_ok = function
+let to_result to_ok v = match force_to_fat v with
   | ValBlk (0, [|v|]) -> Ok (to_ok v)
   | ValBlk (1, [|e|]) -> Error (to_exn e)
   | _ -> assert false
@@ -300,13 +299,16 @@ let result ok = {
 }
 
 let of_option f = function
-| None -> ValInt 0
-| Some c -> ValBlk (0, [|f c|])
+| None -> of_int 0
+| Some c -> of_fat @@ ValBlk (0, [|f c|])
 
-let to_option f = function
-| ValInt 0 -> None
-| ValBlk (0, [|c|]) -> Some (f c)
-| _ -> assert false
+let to_option f v =
+  if is_int v then
+    let () = assert (unsafe_to_int v = 0) in
+    None
+  else match unsafe_to_fat v with
+    | ValBlk (0, [|c|]) -> Some (f c)
+    | _ -> assert false
 
 let option r = {
   r_of = (fun l -> of_option r.r_of l);
@@ -317,13 +319,13 @@ let of_pp c = of_ext val_pp c
 let to_pp c = to_ext val_pp c
 let pp = repr_ext val_pp
 
-let of_tuple cl = ValBlk (0, cl)
-let to_tuple = function
+let of_tuple cl = of_fat @@ ValBlk (0, cl)
+let to_tuple v = match force_to_fat v with
 | ValBlk (0, cl) -> cl
 | _ -> assert false
 
-let of_pair f g (x, y) = ValBlk (0, [|f x; g y|])
-let to_pair f g = function
+let of_pair f g (x, y) = of_fat @@ ValBlk (0, [|f x; g y|])
+let to_pair f g v = match force_to_fat v with
 | ValBlk (0, [|x; y|]) -> (f x, g y)
 | _ -> assert false
 let pair r0 r1 = {
@@ -331,8 +333,8 @@ let pair r0 r1 = {
   r_to = (fun p -> to_pair r0.r_to r1.r_to p);
 }
 
-let of_triple f g h (x, y, z) = ValBlk (0, [|f x; g y; h z|])
-let to_triple f g h = function
+let of_triple f g h (x, y, z) = of_fat @@ ValBlk (0, [|f x; g y; h z|])
+let to_triple f g h v = match force_to_fat v with
 | ValBlk (0, [|x; y; z|]) -> (f x, g y, h z)
 | _ -> assert false
 let triple r0 r1 r2 = {
@@ -340,8 +342,8 @@ let triple r0 r1 r2 = {
   r_to = (fun p -> to_triple r0.r_to r1.r_to r2.r_to p);
 }
 
-let of_array f vl = ValBlk (0, Array.map f vl)
-let to_array f = function
+let of_array f vl = of_fat @@ ValBlk (0, Array.map f vl)
+let to_array f v = match force_to_fat v with
 | ValBlk (0, vl) -> Array.map f vl
 | _ -> assert false
 let array r = {
@@ -349,8 +351,8 @@ let array r = {
   r_to = (fun l -> to_array r.r_to l);
 }
 
-let of_block (n, args) = ValBlk (n, args)
-let to_block = function
+let of_block (n, args) = of_fat @@ ValBlk (n, args)
+let to_block v = match force_to_fat v with
 | ValBlk (n, args) -> (n, args)
 | _ -> assert false
 
@@ -359,9 +361,9 @@ let block = {
   r_to = to_block;
 }
 
-let of_open (kn, args) = ValOpn (kn, args)
+let of_open (kn, args) = of_fat @@ ValOpn (kn, args)
 
-let to_open = function
+let to_open v = match force_to_fat v with
 | ValOpn (kn, args) -> (kn, args)
 | _ -> assert false
 
@@ -451,12 +453,12 @@ let to_instance c = to_ext val_instance c
 let instance = repr_ext val_instance
 
 let of_reference = let open Names.GlobRef in function
-| VarRef id -> ValBlk (0, [| of_ident id |])
-| ConstRef cst -> ValBlk (1, [| of_constant cst |])
-| IndRef ind -> ValBlk (2, [| of_inductive ind |])
-| ConstructRef cstr -> ValBlk (3, [| of_constructor cstr |])
+| VarRef id -> of_fat @@ ValBlk (0, [| of_ident id |])
+| ConstRef cst -> of_fat @@ ValBlk (1, [| of_constant cst |])
+| IndRef ind -> of_fat @@ ValBlk (2, [| of_inductive ind |])
+| ConstructRef cstr -> of_fat @@ ValBlk (3, [| of_constructor cstr |])
 
-let to_reference = let open Names.GlobRef in function
+let to_reference v = let open Names.GlobRef in match force_to_fat v with
 | ValBlk (0, [| id |]) -> VarRef (to_ident id)
 | ValBlk (1, [| cst |]) -> ConstRef (to_constant cst)
 | ValBlk (2, [| ind |]) -> IndRef (to_inductive ind)
@@ -467,3 +469,41 @@ let reference = {
   r_of = of_reference;
   r_to = to_reference;
 }
+
+let of_strategy_level = let open Conv_oracle in function
+| Expand -> of_int 0
+| Opaque -> of_int 1
+| Level n -> of_fat @@ ValBlk (0, [| of_int n |])
+
+let to_strategy_level v = let open Conv_oracle in
+  if is_int v then
+    match unsafe_to_int v with
+    | 0 -> Expand
+    | 1 -> Opaque
+    | _ -> assert false
+  else match unsafe_to_fat v with
+    | ValBlk (0, [| n |]) -> Level (to_int n)
+    | _ -> assert false
+
+let strategy_level = {
+  r_of = of_strategy_level;
+  r_to = to_strategy_level;
+}
+
+let err_notfocussed =
+  LtacError (rocq_core "Not_focussed", [||])
+
+let err_outofbounds =
+  LtacError (rocq_core "Out_of_bounds", [||])
+
+let err_notfound =
+  LtacError (rocq_core "Not_found", [||])
+
+let err_matchfailure =
+  LtacError (rocq_core "Match_failure", [||])
+
+let err_division_by_zero =
+  LtacError (rocq_core "Division_by_zero", [||])
+
+let err_invalid_arg msg =
+  LtacError (rocq_core "Invalid_argument", [|of_option of_pp (Some msg)|])
diff --git a/plugins/ltac2/tac2interp.ml b/plugins/ltac2/tac2interp.ml
index e5542278ad6f..3acc29eba478 100644
--- a/plugins/ltac2/tac2interp.ml
+++ b/plugins/ltac2/tac2interp.ml
@@ -53,27 +53,37 @@ let return = Proofview.tclUNIT
 exception NoMatch
 
 let match_ctor_against ctor v =
-  match ctor, v with
-  | { cindx = Open ctor }, ValOpn (ctor', vs) ->
+  match ctor with
+  | { cindx = Open ctor } ->
+    begin match force_to_fat v with
+    | ValOpn (ctor', vs) ->
     if KerName.equal ctor ctor' then vs
     else raise NoMatch
-  | { cindx = Open _ }, _ -> assert false
-  | { cnargs = 0; cindx = Closed i }, ValInt i' ->
-    if Int.equal i i' then [| |]
-    else raise NoMatch
-  | { cnargs = 0; cindx = Closed _ }, ValBlk _ -> raise NoMatch
-  | _, ValInt _ -> raise NoMatch
-  | { cindx = Closed i }, ValBlk (i', vs) ->
-    if Int.equal i i' then vs
+    | _ -> assert false
+    end
+  | { cnargs = 0; cindx = Closed i } ->
+    if is_int v then
+      let i' = unsafe_to_int v in
+      if Int.equal i i' then [| |]
+      else raise NoMatch
     else raise NoMatch
-  | { cindx = Closed _ }, ValOpn _ -> assert false
-  | _, (ValStr _ | ValCls _ | ValExt _) -> assert false
+  | { cindx = Closed i } ->
+    if is_int v then raise NoMatch
+    else begin match unsafe_to_fat v with
+      | ValBlk (i', vs) ->
+        if Int.equal i i' then vs
+        else raise NoMatch
+      | _ -> assert false
+    end
 
 let check_atom_against atm v =
-  match atm, v with
-  | AtmInt n, ValInt n' -> if not (Int.equal n n') then raise NoMatch
-  | AtmStr s, ValStr s' -> if not (String.equal s (Bytes.unsafe_to_string s')) then raise NoMatch
-  | (AtmInt _ | AtmStr _), _ -> assert false
+  match atm with
+  | AtmInt n ->
+    let n' = force_to_int v in
+    if not (Int.equal n n') then raise NoMatch
+  | AtmStr s ->
+    let s' = Tac2ffi.to_bytes v in
+    if not (String.equal s (Bytes.unsafe_to_string s')) then raise NoMatch
 
 let rec match_pattern_against ist pat v =
   match pat with
@@ -176,7 +186,7 @@ and interp_closure f =
 
 and interp_case ist e cse0 cse1 =
   if Valexpr.is_int e then
-    interp ist cse0.(Tac2ffi.to_int e)
+    interp ist cse0.(unsafe_to_int e)
   else
     let (n, args) = Tac2ffi.to_block e in
     let (ids, e) = cse1.(n) in
diff --git a/plugins/ltac2/tac2stdlib.ml b/plugins/ltac2/tac2stdlib.ml
index abddfb6c1519..f036e6e0496a 100644
--- a/plugins/ltac2/tac2stdlib.ml
+++ b/plugins/ltac2/tac2stdlib.ml
@@ -32,12 +32,15 @@ let to_name c = match Value.to_option Value.to_ident c with
 
 let name = make_to_repr to_name
 
-let to_occurrences = function
-| ValInt 0 -> AllOccurrences
-| ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list Value.to_int vl)
-| ValInt 1 -> NoOccurrences
-| ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list Value.to_int vl)
-| _ -> assert false
+let to_occurrences v =
+  if is_int v then match unsafe_to_int v with
+    | 0 -> AllOccurrences
+    | 1 -> NoOccurrences
+    | _ -> assert false
+  else match unsafe_to_fat v with
+    | ValBlk (0, [| vl |]) -> AllOccurrencesBut (Value.to_list Value.to_int vl)
+    | ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list Value.to_int vl)
+    | _ -> assert false
 
 let occurrences = make_to_repr to_occurrences
 
@@ -60,9 +63,10 @@ let to_clause v = match Value.to_tuple v with
 
 let clause = make_to_repr to_clause
 
-let to_red_strength = function
-  | ValInt 0 -> Norm
-  | ValInt 1 -> Head
+let to_red_strength v =
+  match force_to_int v with
+  | 0 -> Norm
+  | 1 -> Head
   | _ -> assert false
 
 let to_red_flag v : Tac2types.red_flag = match Value.to_tuple v with
@@ -95,23 +99,29 @@ let rec to_intro_pattern v = match Value.to_block v with
 | (2, [| act |]) -> IntroAction (to_intro_pattern_action act)
 | _ -> assert false
 
-and to_intro_pattern_naming = function
-| ValBlk (0, [| id |]) -> IntroIdentifier (Value.to_ident id)
-| ValBlk (1, [| id |]) -> IntroFresh (Value.to_ident id)
-| ValInt 0 -> IntroAnonymous
-| _ -> assert false
-
-and to_intro_pattern_action = function
-| ValInt 0 -> IntroWildcard
-| ValBlk (0, [| op |]) -> IntroOrAndPattern (to_or_and_intro_pattern op)
-| ValBlk (1, [| inj |]) ->
-  let map ipat = to_intro_pattern ipat in
-  IntroInjection (Value.to_list map inj)
-| ValBlk (2, [| c; ipat |]) ->
-  let c = Value.to_fun1 Value.of_unit Value.to_constr c in
-  IntroApplyOn (c, to_intro_pattern ipat)
-| ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b)
-| _ -> assert false
+and to_intro_pattern_naming v =
+  if is_int v then
+    let () = assert (unsafe_to_int v = 0) in
+    IntroAnonymous
+  else match unsafe_to_fat v with
+    | ValBlk (0, [| id |]) -> IntroIdentifier (Value.to_ident id)
+    | ValBlk (1, [| id |]) -> IntroFresh (Value.to_ident id)
+    | _ -> assert false
+
+and to_intro_pattern_action v =
+  if is_int v then
+    let () = assert (unsafe_to_int v = 0) in
+    IntroWildcard
+  else match unsafe_to_fat v with
+    | ValBlk (0, [| op |]) -> IntroOrAndPattern (to_or_and_intro_pattern op)
+    | ValBlk (1, [| inj |]) ->
+      let map ipat = to_intro_pattern ipat in
+      IntroInjection (Value.to_list map inj)
+    | ValBlk (2, [| c; ipat |]) ->
+      let c = Value.to_fun1 Value.of_unit Value.to_constr c in
+      IntroApplyOn (c, to_intro_pattern ipat)
+    | ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b)
+    | _ -> assert false
 
 and to_or_and_intro_pattern v = match Value.to_block v with
 | (0, [| ill |]) ->
@@ -187,12 +197,15 @@ let to_assertion v = match Value.to_block v with
 
 let assertion = make_to_repr to_assertion
 
-let to_multi = function
-| ValBlk (0, [| n |]) -> Precisely (Value.to_int n)
-| ValBlk (1, [| n |]) -> UpTo (Value.to_int n)
-| ValInt 0 -> RepeatStar
-| ValInt 1 -> RepeatPlus
-| _ -> assert false
+let to_multi v =
+  if is_int v then match unsafe_to_int v with
+    | 0 -> RepeatStar
+    | 1 -> RepeatPlus
+    | _ -> assert false
+  else match unsafe_to_fat v with
+    | ValBlk (0, [| n |]) -> Precisely (Value.to_int n)
+    | ValBlk (1, [| n |]) -> UpTo (Value.to_int n)
+    | _ -> assert false
 
 let to_rewriting v = match Value.to_tuple v with
 | [| orient; repeat; c |] ->
@@ -227,12 +240,16 @@ let to_inversion_kind v = match Value.to_int v with
 
 let inversion_kind = make_to_repr to_inversion_kind
 
-let to_move_location = function
-| ValInt 0 -> Logic.MoveFirst
-| ValInt 1 -> Logic.MoveLast
-| ValBlk (0, [|id|]) -> Logic.MoveAfter (Value.to_ident id)
-| ValBlk (1, [|id|]) -> Logic.MoveBefore (Value.to_ident id)
-| _ -> assert false
+
+let to_move_location v =
+  if is_int v then match unsafe_to_int v with
+    | 0 -> Logic.MoveFirst
+    | 1 -> Logic.MoveLast
+    | _ -> assert false
+  else match unsafe_to_fat v with
+    | ValBlk (0, [|id|]) -> Logic.MoveAfter (Value.to_ident id)
+    | ValBlk (1, [|id|]) -> Logic.MoveBefore (Value.to_ident id)
+    | _ -> assert false
 
 let move_location = make_to_repr to_move_location
 
diff --git a/plugins/ltac2/tac2val.ml b/plugins/ltac2/tac2val.ml
index dda1d6bd7131..378261380a38 100644
--- a/plugins/ltac2/tac2val.ml
+++ b/plugins/ltac2/tac2val.ml
@@ -18,9 +18,12 @@ type ('a, _) arity0 =
 
 type tag = int
 
-type valexpr =
-| ValInt of int
-  (** Immediate integers *)
+(** Immediate integers are unboxed, other values are [valfat]. *)
+type valexpr
+
+type closure = MLTactic : (valexpr, 'v) arity0 * Tac2expr.frame option * 'v -> closure
+
+type valfat =
 | ValBlk of tag * valexpr array
   (** Structured blocks *)
 | ValStr of Bytes.t
@@ -29,10 +32,18 @@ type valexpr =
   (** Closures *)
 | ValOpn of KerName.t * valexpr array
   (** Open constructors *)
-| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
+| ValExt : 'a Tac2dyn.Val.tag * 'a -> valfat
   (** Arbitrary data *)
 
-and closure = MLTactic : (valexpr, 'v) arity0 * Tac2expr.frame option * 'v -> closure
+external of_int : int -> valexpr = "%identity"
+external of_fat : valfat -> valexpr = "%identity"
+external unsafe_to_int : valexpr -> int = "%identity"
+external unsafe_to_fat : valexpr -> valfat = "%identity"
+external is_int : valexpr -> bool = "%obj_is_int"
+
+let force_to_int v = if is_int v then unsafe_to_int v else assert false
+
+let force_to_fat v = if is_int v then assert false else unsafe_to_fat v
 
 let arity_one = OneAty
 let arity_suc a = AddAty a
@@ -41,40 +52,39 @@ type 'a arity = (valexpr, 'a) arity0
 
 let mk_closure arity f = MLTactic (arity, None, f)
 
-let mk_closure_val arity f = ValCls (mk_closure arity f)
+let mk_closure_val arity f = of_fat @@ ValCls (mk_closure arity f)
 
 module Valexpr =
 struct
 
 type t = valexpr
 
-let is_int = function
-| ValInt _ -> true
-| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> false
+let is_int = is_int
 
-let tag v = match v with
-| ValBlk (n, _) -> n
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
-  CErrors.anomaly (Pp.str "Unexpected value shape")
+let tag v =
+  match force_to_fat v with
+  | ValBlk (n, _) -> n
+  | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+    CErrors.anomaly (Pp.str "Unexpected value shape")
 
-let field v n = match v with
+let field v n = match force_to_fat v with
 | ValBlk (_, v) -> v.(n)
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+| ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
   CErrors.anomaly (Pp.str "Unexpected value shape")
 
-let set_field v n w = match v with
+let set_field v n w = match force_to_fat v with
 | ValBlk (_, v) -> v.(n) <- w
-| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+| ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
   CErrors.anomaly (Pp.str "Unexpected value shape")
 
-let make_block tag v = ValBlk (tag, v)
-let make_int n = ValInt n
+let make_block tag v = of_fat @@ ValBlk (tag, v)
+let make_int = of_int
 
 end
 
-let to_closure = function
+let to_closure v = match force_to_fat v with
 | ValCls cls -> cls
-| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false
+| ValExt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false
 
 let wrap fr tac = match fr with
   | None -> tac
@@ -82,7 +92,7 @@ let wrap fr tac = match fr with
 
 let rec apply : type a. a arity -> _ -> a -> valexpr list -> valexpr Proofview.tactic =
   fun arity fr f args -> match args, arity with
-  | [], arity -> Proofview.tclUNIT (ValCls (MLTactic (arity, fr, f)))
+  | [], arity -> Proofview.tclUNIT (of_fat @@ ValCls (MLTactic (arity, fr, f)))
   (* A few hardcoded cases for efficiency *)
   | [a0], OneAty -> wrap fr (f a0)
   | [a0; a1], AddAty OneAty -> wrap fr (f a0 a1)
diff --git a/plugins/ltac2/tac2val.mli b/plugins/ltac2/tac2val.mli
index e8acb5ab2e84..ab8383f4d031 100644
--- a/plugins/ltac2/tac2val.mli
+++ b/plugins/ltac2/tac2val.mli
@@ -24,9 +24,10 @@ type tag = int
 
 type closure
 
-type valexpr =
-| ValInt of int
-  (** Immediate integers *)
+(** Immediate integers are unboxed, other values are [valfat]. *)
+type valexpr
+
+type valfat =
 | ValBlk of tag * valexpr array
   (** Structured blocks *)
 | ValStr of Bytes.t
@@ -35,9 +36,19 @@ type valexpr =
   (** Closures *)
 | ValOpn of KerName.t * valexpr array
   (** Open constructors *)
-| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
+| ValExt : 'a Tac2dyn.Val.tag * 'a -> valfat
   (** Arbitrary data *)
 
+(** Exposed as externals in case it helps the compiler *)
+external of_int : int -> valexpr = "%identity"
+external of_fat : valfat -> valexpr = "%identity"
+external unsafe_to_int : valexpr -> int = "%identity"
+external unsafe_to_fat : valexpr -> valfat = "%identity"
+external is_int : valexpr -> bool = "%obj_is_int"
+
+val force_to_int : valexpr -> int
+val force_to_fat : valexpr -> valfat
+
 module Valexpr :
 sig
   type t = valexpr