Parameterizing over parameters in ML functions from Tac2core.

3 files changed, 93 insertions, 136 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 5e475e1d4a..2f349e32af 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -20,6 +20,7 @@ open Proofview.Notations
 (** Standard values *)
 
 module Value = Tac2ffi
+open Value
 
 let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
 let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
@@ -53,10 +54,6 @@ open Core
 
 let v_unit = ValInt 0
 
-let to_block = function
-| ValBlk (_, v) -> v
-| _ -> assert false
-
 let of_name c = match c with
 | Anonymous -> Value.of_option Value.of_ident None
 | Name id -> Value.of_option Value.of_ident (Some id)
@@ -103,7 +100,8 @@ let err_matchfailure bt =
 
 (** Helper functions *)
 
-let thaw bt f = Tac2interp.interp_app bt (Value.to_closure f) [v_unit]
+let thaw bt f = Tac2interp.interp_app bt f [v_unit]
+
 let throw bt e = Proofview.tclLIFT (Proofview.NonLogical.raise (e bt))
 
 let set_bt bt e = match e with
@@ -144,111 +142,95 @@ let define0 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> m
 | _ -> assert false
 end
 
-let define1 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
-| [x] -> f bt x
+let define1 name r0 f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
+| [x] -> f bt (r0.Value.r_to x)
 | _ -> assert false
 end
 
-let define2 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
-| [x; y] -> f bt x y
+let define2 name r0 r1 f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
+| [x; y] -> f bt (r0.Value.r_to x) (r1.Value.r_to y)
 | _ -> assert false
 end
 
-let define3 name f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
-| [x; y; z] -> f bt x y z
+let define3 name r0 r1 r2 f = Tac2env.define_primitive (pname name) begin fun bt arg -> match arg with
+| [x; y; z] -> f bt (r0.Value.r_to x) (r1.Value.r_to y) (r2.Value.r_to z)
 | _ -> assert false
 end
 
 (** Printing *)
 
-let () = define1 "print" begin fun _ pp ->
-  wrap_unit (fun () -> Feedback.msg_notice (Value.to_pp pp))
+let () = define1 "print" pp begin fun _ pp ->
+  wrap_unit (fun () -> Feedback.msg_notice pp)
 end
 
-let () = define1 "message_of_int" begin fun _ n ->
-  let n = Value.to_int n in
-  return (Value.of_pp (int n))
+let () = define1 "message_of_int" int begin fun _ n ->
+  return (Value.of_pp (Pp.int n))
 end
 
-let () = define1 "message_of_string" begin fun _ s ->
-  let s = Value.to_string s in
+let () = define1 "message_of_string" string begin fun _ s ->
   return (Value.of_pp (str (Bytes.to_string s)))
 end
 
-let () = define1 "message_of_constr" begin fun bt c ->
+let () = define1 "message_of_constr" constr begin fun bt c ->
   pf_apply bt begin fun env sigma ->
-    let c = Value.to_constr c in
     let pp = Printer.pr_econstr_env env sigma c in
     return (Value.of_pp pp)
   end
 end
 
-let () = define1 "message_of_ident" begin fun _ c ->
-  let c = Value.to_ident c in
+let () = define1 "message_of_ident" ident begin fun _ c ->
   let pp = Id.print c in
   return (Value.of_pp pp)
 end
 
-let () = define2 "message_concat" begin fun _ m1 m2 ->
-  let m1 = Value.to_pp m1 in
-  let m2 = Value.to_pp m2 in
+let () = define2 "message_concat" pp pp begin fun _ m1 m2 ->
   return (Value.of_pp (Pp.app m1 m2))
 end
 
 (** Array *)
 
-let () = define2 "array_make" begin fun bt n x ->
-  let n = Value.to_int n in
+let () = define2 "array_make" int valexpr begin fun bt n x ->
   if n < 0 || n > Sys.max_array_length then throw bt err_outofbounds
   else wrap (fun () -> ValBlk (0, Array.make n x))
 end
 
-let () = define1 "array_length" begin fun _ v ->
-  let v = to_block v in
+let () = define1 "array_length" block begin fun _ v ->
   return (ValInt (Array.length v))
 end
 
-let () = define3 "array_set" begin fun bt v n x ->
-  let v = to_block v in
-  let n = Value.to_int n in
+let () = define3 "array_set" block int valexpr begin fun bt v n x ->
   if n < 0 || n >= Array.length v then throw bt err_outofbounds
   else wrap_unit (fun () -> v.(n) <- x)
 end
 
-let () = define2 "array_get" begin fun bt v n ->
-  let v = to_block v in
-  let n = Value.to_int n in
+let () = define2 "array_get" block int begin fun bt v n ->
   if n < 0 || n >= Array.length v then throw bt err_outofbounds
   else wrap (fun () -> v.(n))
 end
 
 (** Ident *)
 
-let () = define2 "ident_equal" begin fun _ id1 id2 ->
-  let id1 = Value.to_ident id1 in
-  let id2 = Value.to_ident id2 in
+let () = define2 "ident_equal" ident ident begin fun _ id1 id2 ->
   return (Value.of_bool (Id.equal id1 id2))
 end
 
-let () = define1 "ident_to_string" begin fun _ id ->
-  let id = Value.to_ident id in
+let () = define1 "ident_to_string" ident begin fun _ id ->
   return (Value.of_string (Id.to_string id))
 end
 
-let () = define1 "ident_of_string" begin fun _ s ->
-  let s = Value.to_string s in
+let () = define1 "ident_of_string" string begin fun _ s ->
   let id = try Some (Id.of_string s) with _ -> None in
   return (Value.of_option Value.of_ident id)
 end
 
 (** Int *)
 
-let () = define2 "int_equal" begin fun _ m n ->
-  return (Value.of_bool (Value.to_int m == Value.to_int n))
+let () = define2 "int_equal" int int begin fun _ m n ->
+  return (Value.of_bool (m == n))
 end
 
-let binop n f = define2 n begin fun _ m n ->
-  return (Value.of_int (f (Value.to_int m) (Value.to_int n)))
+let binop n f = define2 n int int begin fun _ m n ->
+  return (Value.of_int (f m m))
 end
 
 let () = binop "int_compare" Int.compare
@@ -256,34 +238,27 @@ let () = binop "int_add" (+)
 let () = binop "int_sub" (-)
 let () = binop "int_mul" ( * )
 
-let () = define1 "int_neg" begin fun _ m ->
-  return (Value.of_int (~- (Value.to_int m)))
+let () = define1 "int_neg" int begin fun _ m ->
+  return (Value.of_int (~- m))
 end
 
 (** String *)
 
-let () = define2 "string_make" begin fun bt n c ->
-  let n = Value.to_int n in
-  let c = Value.to_char c in
+let () = define2 "string_make" int char begin fun bt n c ->
   if n < 0 || n > Sys.max_string_length then throw bt err_outofbounds
   else wrap (fun () -> Value.of_string (Bytes.make n c))
 end
 
-let () = define1 "string_length" begin fun _ s ->
-  return (Value.of_int (Bytes.length (Value.to_string s)))
+let () = define1 "string_length" string begin fun _ s ->
+  return (Value.of_int (Bytes.length s))
 end
 
-let () = define3 "string_set" begin fun bt s n c ->
-  let s = Value.to_string s in
-  let n = Value.to_int n in
-  let c = Value.to_char c in
+let () = define3 "string_set" string int char begin fun bt s n c ->
   if n < 0 || n >= Bytes.length s then throw bt err_outofbounds
   else wrap_unit (fun () -> Bytes.set s n c)
 end
 
-let () = define2 "string_get" begin fun bt s n ->
-  let s = Value.to_string s in
-  let n = Value.to_int n in
+let () = define2 "string_get" string int begin fun bt s n ->
   if n < 0 || n >= Bytes.length s then throw bt err_outofbounds
   else wrap (fun () -> Value.of_char (Bytes.get s n))
 end
@@ -291,8 +266,7 @@ end
 (** Terms *)
 
 (** constr -> constr *)
-let () = define1 "constr_type" begin fun bt c ->
-  let c = Value.to_constr c in
+let () = define1 "constr_type" constr begin fun bt c ->
   let get_type env sigma =
   Proofview.V82.wrap_exceptions begin fun () ->
     let (sigma, t) = Typing.type_of env sigma c in
@@ -303,18 +277,15 @@ let () = define1 "constr_type" begin fun bt c ->
 end
 
 (** constr -> constr *)
-let () = define2 "constr_equal" begin fun _ c1 c2 ->
-  let c1 = Value.to_constr c1 in
-  let c2 = Value.to_constr c2 in
+let () = define2 "constr_equal" constr constr begin fun _ c1 c2 ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let b = EConstr.eq_constr sigma c1 c2 in
   Proofview.tclUNIT (Value.of_bool b)
 end
 
-let () = define1 "constr_kind" begin fun _ c ->
+let () = define1 "constr_kind" constr begin fun _ c ->
   let open Constr in
   Proofview.tclEVARMAP >>= fun sigma ->
-  let c = Value.to_constr c in
   return begin match EConstr.kind sigma c with
   | Rel n ->
     ValBlk (0, [|Value.of_int n|])
@@ -406,7 +377,7 @@ let () = define1 "constr_kind" begin fun _ c ->
   end
 end
 
-let () = define1 "constr_make" begin fun _ knd ->
+let () = define1 "constr_make" valexpr begin fun _ knd ->
   let open Constr in
   let c = match knd with
   | ValBlk (0, [|n|]) ->
@@ -486,8 +457,7 @@ let () = define1 "constr_make" begin fun _ knd ->
   return (Value.of_constr c)
 end
 
-let () = define1 "constr_check" begin fun bt c ->
-  let c = Value.to_constr c in
+let () = define1 "constr_check" constr begin fun bt c ->
   pf_apply bt begin fun env sigma ->
     try
       let (sigma, _) = Typing.type_of env sigma c in
@@ -499,27 +469,19 @@ let () = define1 "constr_check" begin fun bt c ->
   end
 end
 
-let () = define3 "constr_substnl" begin fun _ subst k c ->
-  let subst = Value.to_list Value.to_constr subst in
-  let k = Value.to_int k in
-  let c = Value.to_constr c in
+let () = define3 "constr_substnl" (list constr) int constr begin fun _ subst k c ->
   let ans = EConstr.Vars.substnl subst k c in
   return (Value.of_constr ans)
 end
 
-let () = define3 "constr_closenl" begin fun _ ids k c ->
-  let ids = Value.to_list Value.to_ident ids in
-  let k = Value.to_int k in
-  let c = Value.to_constr c in
+let () = define3 "constr_closenl" (list ident) int constr begin fun _ ids k c ->
   let ans = EConstr.Vars.substn_vars k ids c in
   return (Value.of_constr ans)
 end
 
 (** Patterns *)
 
-let () = define2 "pattern_matches" begin fun bt pat c ->
-  let pat = Value.to_pattern pat in
-  let c = Value.to_constr c in
+let () = define2 "pattern_matches" pattern constr begin fun bt pat c ->
   pf_apply bt begin fun env sigma ->
     let ans =
       try Some (Constr_matching.matches env sigma pat c)
@@ -535,9 +497,7 @@ let () = define2 "pattern_matches" begin fun bt pat c ->
   end
 end
 
-let () = define2 "pattern_matches_subterm" begin fun bt pat c ->
-  let pat = Value.to_pattern pat in
-  let c = Value.to_constr c in
+let () = define2 "pattern_matches_subterm" pattern constr begin fun bt pat c ->
   let open Constr_matching in
   let rec of_ans s = match IStream.peek s with
   | IStream.Nil -> Proofview.tclZERO (err_matchfailure bt)
@@ -553,9 +513,7 @@ let () = define2 "pattern_matches_subterm" begin fun bt pat c ->
   end
 end
 
-let () = define2 "pattern_matches_vect" begin fun bt pat c ->
-  let pat = Value.to_pattern pat in
-  let c = Value.to_constr c in
+let () = define2 "pattern_matches_vect" pattern constr begin fun bt pat c ->
   pf_apply bt begin fun env sigma ->
     let ans =
       try Some (Constr_matching.matches env sigma pat c)
@@ -571,9 +529,7 @@ let () = define2 "pattern_matches_vect" begin fun bt pat c ->
   end
 end
 
-let () = define2 "pattern_matches_subterm_vect" begin fun bt pat c ->
-  let pat = Value.to_pattern pat in
-  let c = Value.to_constr c in
+let () = define2 "pattern_matches_subterm_vect" pattern constr begin fun bt pat c ->
   let open Constr_matching in
   let rec of_ans s = match IStream.peek s with
   | IStream.Nil -> Proofview.tclZERO (err_matchfailure bt)
@@ -589,17 +545,16 @@ let () = define2 "pattern_matches_subterm_vect" begin fun bt pat c ->
   end
 end
 
-let () = define2 "pattern_instantiate" begin fun _ ctx c ->
-  let ctx = EConstr.Unsafe.to_constr (Value.to_constr ctx) in
-  let c = EConstr.Unsafe.to_constr (Value.to_constr c) in
+let () = define2 "pattern_instantiate" constr constr begin fun _ ctx c ->
+  let ctx = EConstr.Unsafe.to_constr ctx in
+  let c = EConstr.Unsafe.to_constr c in
   let ans = Termops.subst_meta [Constr_matching.special_meta, c] ctx in
   return (Value.of_constr (EConstr.of_constr ans))
 end
 
 (** Error *)
 
-let () = define1 "throw" begin fun bt e ->
-  let (e, info) = Value.to_exn e in
+let () = define1 "throw" exn begin fun bt (e, info) ->
   let e = set_bt bt e in
   Proofview.tclLIFT (Proofview.NonLogical.raise ~info e)
 end
@@ -607,38 +562,37 @@ end
 (** Control *)
 
 (** exn -> 'a *)
-let () = define1 "zero" begin fun bt e ->
-  let (e, info) = Value.to_exn e in
+let () = define1 "zero" exn begin fun bt (e, info) ->
   let e = set_bt bt e in
   Proofview.tclZERO ~info e
 end
 
 (** (unit -> 'a) -> (exn -> 'a) -> 'a *)
-let () = define2 "plus" begin fun bt x k ->
-  Proofview.tclOR (thaw bt x) (fun e -> Tac2interp.interp_app bt (Value.to_closure k) [Value.of_exn e])
+let () = define2 "plus" closure closure begin fun bt x k ->
+  Proofview.tclOR (thaw bt x) (fun e -> Tac2interp.interp_app bt k [Value.of_exn e])
 end
 
 (** (unit -> 'a) -> 'a *)
-let () = define1 "once" begin fun bt f ->
+let () = define1 "once" closure begin fun bt f ->
   Proofview.tclONCE (thaw bt f)
 end
 
 (** (unit -> unit) list -> unit *)
-let () = define1 "dispatch" begin fun bt l ->
-  let l = Value.to_list (fun f -> Proofview.tclIGNORE (thaw bt f)) l in
+let () = define1 "dispatch" (list closure) begin fun bt l ->
+  let l = List.map (fun f -> Proofview.tclIGNORE (thaw bt f)) l in
   Proofview.tclDISPATCH l >>= fun () -> return v_unit
 end
 
 (** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *)
-let () = define3 "extend" begin fun bt lft tac rgt ->
-  let lft = Value.to_list (fun f -> Proofview.tclIGNORE (thaw bt f)) lft in
+let () = define3 "extend" (list closure) closure (list closure) begin fun bt lft tac rgt ->
+  let lft = List.map (fun f -> Proofview.tclIGNORE (thaw bt f)) lft in
   let tac = Proofview.tclIGNORE (thaw bt tac) in
-  let rgt = Value.to_list (fun f -> Proofview.tclIGNORE (thaw bt f)) rgt in
+  let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw bt f)) rgt in
   Proofview.tclEXTEND lft tac rgt >>= fun () -> return v_unit
 end
 
 (** (unit -> unit) -> unit *)
-let () = define1 "enter" begin fun bt f ->
+let () = define1 "enter" closure begin fun bt f ->
   let f = Proofview.tclIGNORE (thaw bt f) in
   Proofview.tclINDEPENDENT f >>= fun () -> return v_unit
 end
@@ -648,7 +602,7 @@ let e_var = Id.of_string "e"
 let prm_apply_kont_h = pname "apply_kont"
 
 (** (unit -> 'a) -> ('a * ('exn -> 'a)) result *)
-let () = define1 "case" begin fun bt f ->
+let () = define1 "case" closure begin fun bt f ->
   Proofview.tclCASE (thaw bt f) >>= begin function
   | Proofview.Next (x, k) ->
     let k = {
@@ -663,16 +617,13 @@ let () = define1 "case" begin fun bt f ->
 end
 
 (** 'a kont -> exn -> 'a *)
-let () = define2 "apply_kont" begin fun bt k e ->
-  let (e, info) = Value.to_exn e in
+let () = define2 "apply_kont" (repr_ext val_kont) exn begin fun bt k (e, info) ->
   let e = set_bt bt e in
-  (Value.to_ext Value.val_kont k) (e, info)
+  k (e, info)
 end
 
 (** int -> int -> (unit -> 'a) -> 'a *)
-let () = define3 "focus" begin fun bt i j tac ->
-  let i = Value.to_int i in
-  let j = Value.to_int j in
+let () = define3 "focus" int int closure begin fun bt i j tac ->
   Proofview.tclFOCUS i j (thaw bt tac)
 end
 
@@ -686,8 +637,8 @@ let () = define0 "shelve_unifiable" begin fun _ ->
   Proofview.shelve_unifiable >>= fun () -> return v_unit
 end
 
-let () = define1 "new_goal" begin fun bt ev ->
-  let ev = Evar.unsafe_of_int (Value.to_int ev) in
+let () = define1 "new_goal" int begin fun bt ev ->
+  let ev = Evar.unsafe_of_int ev in
   Proofview.tclEVARMAP >>= fun sigma ->
   if Evd.mem sigma ev then
     Proofview.Unsafe.tclNEWGOALS [ev] <*> Proofview.tclUNIT v_unit
@@ -704,8 +655,7 @@ let () = define0 "goal" begin fun bt ->
 end
 
 (** ident -> constr *)
-let () = define1 "hyp" begin fun bt id ->
-  let id = Value.to_ident id in
+let () = define1 "hyp" ident begin fun bt id ->
   pf_apply bt begin fun env _ ->
     let mem = try ignore (Environ.lookup_named id env); true with Not_found -> false in
     if mem then return (Value.of_constr (EConstr.mkVar id))
@@ -732,7 +682,7 @@ let () = define0 "hyps" begin fun bt ->
 end
 
 (** (unit -> constr) -> unit *)
-let () = define1 "refine" begin fun bt c ->
+let () = define1 "refine" closure begin fun bt c ->
   let c = thaw bt c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in
   Proofview.Goal.enter begin fun gl ->
     let gl = Proofview.Goal.assume gl in
@@ -740,8 +690,7 @@ let () = define1 "refine" begin fun bt c ->
   end >>= fun () -> return v_unit
 end
 
-let () = define2 "with_holes" begin fun bt x f ->
-  let f = Value.to_closure f in
+let () = define2 "with_holes" closure closure begin fun bt x f ->
   Proofview.tclEVARMAP >>= fun sigma0 ->
   thaw bt x >>= fun ans ->
   Proofview.tclEVARMAP >>= fun sigma ->
@@ -749,18 +698,16 @@ let () = define2 "with_holes" begin fun bt x f ->
   Tacticals.New.tclWITHHOLES false (Tac2interp.interp_app bt f [ans]) sigma
 end
 
-let () = define1 "progress" begin fun bt f ->
+let () = define1 "progress" closure begin fun bt f ->
   Proofview.tclPROGRESS (thaw bt f)
 end
 
-let () = define2 "abstract" begin fun bt id f ->
-  let id = Value.to_option Value.to_ident id in
+let () = define2 "abstract" (option ident) closure begin fun bt id f ->
   Tactics.tclABSTRACT id (Proofview.tclIGNORE (thaw bt f)) >>= fun () ->
   return v_unit
 end
 
-let () = define2 "time" begin fun bt s f ->
-  let s = Value.to_option Value.to_string s in
+let () = define2 "time" (option string) closure begin fun bt s f ->
   Proofview.tclTIME s (thaw bt f)
 end
 
@@ -770,21 +717,17 @@ end
 
 (** Fresh *)
 
-let () = define2 "fresh_free_union" begin fun _ set1 set2 ->
-  let set1 = Value.to_ext Value.val_free set1 in
-  let set2 = Value.to_ext Value.val_free set2 in
+let () = define2 "fresh_free_union" (repr_ext val_free) (repr_ext val_free) begin fun _ set1 set2 ->
   let ans = Id.Set.union set1 set2 in
   return (Value.of_ext Value.val_free ans)
 end
 
-let () = define1 "fresh_free_of_ids" begin fun _ ids ->
-  let ids = Value.to_list Value.to_ident ids in
+let () = define1 "fresh_free_of_ids" (list ident) begin fun _ ids ->
   let free = List.fold_right Id.Set.add ids Id.Set.empty in
   return (Value.of_ext Value.val_free free)
 end
 
-let () = define1 "fresh_free_of_constr" begin fun _ c ->
-  let c = Value.to_constr c in
+let () = define1 "fresh_free_of_constr" constr begin fun _ c ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let rec fold accu c = match EConstr.kind sigma c with
   | Constr.Var id -> Id.Set.add id accu
@@ -794,9 +737,7 @@ let () = define1 "fresh_free_of_constr" begin fun _ c ->
   return (Value.of_ext Value.val_free ans)
 end
 
-let () = define2 "fresh_fresh" begin fun _ avoid id ->
-  let avoid = Value.to_ext Value.val_free avoid in
-  let id = Value.to_ident id in
+let () = define2 "fresh_fresh" (repr_ext val_free) ident begin fun _ avoid id ->
   let nid = Namegen.next_ident_away_from id (fun id -> Id.Set.mem id avoid) in
   return (Value.of_ident nid)
 end
@@ -999,7 +940,7 @@ let add_scope s f =
 
 let rec pr_scope = function
 | SexprStr (_, s) -> qstring s
-| SexprInt (_, n) -> int n
+| SexprInt (_, n) -> Pp.int n
 | SexprRec (_, (_, na), args) ->
   let na = match na with
   | None -> str "_"
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index c3f535c1bc..3e3dd362f7 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -49,6 +49,12 @@ exception LtacError of KerName.t * valexpr array * backtrace
 
 (** Conversion functions *)
 
+let valexpr = {
+  r_of = (fun obj -> obj);
+  r_to = (fun obj -> obj);
+  r_id = true;
+}
+
 let of_unit () = ValInt 0
 
 let to_unit = function
@@ -216,6 +222,12 @@ let array r = {
   r_id = false;
 }
 
+let block = {
+  r_of = of_tuple;
+  r_to = to_tuple;
+  r_id = false;
+}
+
 let of_constant c = of_ext val_constant c
 let to_constant c = to_ext val_constant c
 let constant = repr_ext val_constant
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index fe813b0e35..1789a8932f 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -64,6 +64,8 @@ val of_closure : closure -> valexpr
 val to_closure : valexpr -> closure
 val closure : closure repr
 
+val block : valexpr array repr
+
 val of_array : ('a -> valexpr) -> 'a array -> valexpr
 val to_array : (valexpr -> 'a) -> valexpr -> 'a array
 val array : 'a repr -> 'a array repr
@@ -95,6 +97,8 @@ val of_ext : 'a Val.tag -> 'a -> valexpr
 val to_ext : 'a Val.tag -> valexpr -> 'a
 val repr_ext : 'a Val.tag -> 'a repr
 
+val valexpr : valexpr repr
+
 (** {5 Dynamic tags} *)
 
 val val_constr : EConstr.t Val.tag