3 files changed, 7 insertions, 7 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 118bea0f8e..5b752840a4 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -691,7 +691,7 @@ let interp_constr flags ist (c, _) =
   Proofview.V82.wrap_exceptions begin fun () ->
     let ist = to_lvar ist in
     let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in
-    let c = ValExt (Val.Dyn (Value.val_constr, c)) in
+    let c = ValExt (Value.val_constr, c) in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT c
   end
@@ -714,7 +714,7 @@ let () =
   define_ml_object Stdarg.wit_open_constr obj
 
 let () =
-  let interp _ id = return (ValExt (Val.Dyn (Value.val_ident, id))) in
+  let interp _ id = return (ValExt (Value.val_ident, id)) in
   let obj = {
     ml_type = t_ident;
     ml_interp = interp;
@@ -722,7 +722,7 @@ let () =
   define_ml_object Stdarg.wit_ident obj
 
 let () =
-  let interp _ c = return (ValExt (Val.Dyn (Value.val_pattern, c))) in
+  let interp _ c = return (ValExt (Value.val_pattern, c)) in
   let obj = {
     ml_type = t_pattern;
     ml_interp = interp;
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 78611d51ca..0c9112d902 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -186,7 +186,7 @@ type valexpr =
   (** Closures *)
 | ValOpn of KerName.t * valexpr array
   (** Open constructors *)
-| ValExt of Geninterp.Val.t
+| ValExt : 'a Geninterp.Val.typ * 'a -> valexpr
   (** Arbitrary data *)
 
 and closure = {
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index b506a578b1..a9a0f5a479 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -33,7 +33,7 @@ let val_univ = Val.create "ltac2:universe"
 let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.typ =
   Val.create "ltac2:kont"
 
-let extract_val (type a) (tag : a Val.typ) (Val.Dyn (tag', v)) : a =
+let extract_val (type a) (type b) (tag : a Val.typ) (tag' : b Val.typ) (v : b) : a =
 match Val.eq tag tag' with
 | None -> assert false
 | Some Refl -> v
@@ -78,10 +78,10 @@ let rec to_list f = function
 | _ -> assert false
 
 let of_ext tag c =
-  ValExt (Val.Dyn (tag, c))
+  ValExt (tag, c)
 
 let to_ext tag = function
-| ValExt e -> extract_val tag e
+| ValExt (tag', e) -> extract_val tag tag' e
 | _ -> assert false
 
 let of_constr c = of_ext val_constr c