Abstracting away the primitive functions on valexpr datatype.

7 files changed, 214 insertions, 161 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 1917fa5f66..9e3cefc6f5 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -53,7 +53,8 @@ end
 
 open Core
 
-let v_unit = ValInt 0
+let v_unit = Value.of_unit ()
+let v_blk = Valexpr.make_block
 
 let of_name c = match c with
 | Anonymous -> Value.of_option Value.of_ident None
@@ -82,8 +83,8 @@ let to_rec_declaration (nas, ts, cs) =
   Value.to_array Value.to_constr cs)
 
 let of_result f = function
-| Inl c -> ValBlk (0, [|f c|])
-| Inr e -> ValBlk (1, [|Value.of_exn e|])
+| Inl c -> v_blk 0 [|f c|]
+| Inr e -> v_blk 1 [|Value.of_exn e|]
 
 (** Stdlib exceptions *)
 
@@ -209,19 +210,19 @@ end
 
 let () = define2 "array_make" int valexpr begin fun n x ->
   if n < 0 || n > Sys.max_array_length then throw err_outofbounds
-  else wrap (fun () -> ValBlk (0, Array.make n x))
+  else wrap (fun () -> v_blk 0 (Array.make n x))
 end
 
-let () = define1 "array_length" block begin fun v ->
-  return (ValInt (Array.length v))
+let () = define1 "array_length" block begin fun (_, v) ->
+  return (Value.of_int (Array.length v))
 end
 
-let () = define3 "array_set" block int valexpr begin fun v n x ->
+let () = define3 "array_set" block int valexpr begin fun (_, v) n x ->
   if n < 0 || n >= Array.length v then throw err_outofbounds
   else wrap_unit (fun () -> v.(n) <- x)
 end
 
-let () = define2 "array_get" block int begin fun v n ->
+let () = define2 "array_get" block int begin fun (_, v) n ->
   if n < 0 || n >= Array.length v then throw err_outofbounds
   else wrap (fun () -> v.(n))
 end
@@ -306,167 +307,167 @@ let () = define1 "constr_kind" constr begin fun c ->
   Proofview.tclEVARMAP >>= fun sigma ->
   return begin match EConstr.kind sigma c with
   | Rel n ->
-    ValBlk (0, [|Value.of_int n|])
+    v_blk 0 [|Value.of_int n|]
   | Var id ->
-    ValBlk (1, [|Value.of_ident id|])
+    v_blk 1 [|Value.of_ident id|]
   | Meta n ->
-    ValBlk (2, [|Value.of_int n|])
+    v_blk 2 [|Value.of_int n|]
   | Evar (evk, args) ->
-    ValBlk (3, [|
+    v_blk 3 [|
       Value.of_int (Evar.repr evk);
       Value.of_array Value.of_constr args;
-    |])
+    |]
   | Sort s ->
-    ValBlk (4, [|Value.of_ext Value.val_sort s|])
+    v_blk 4 [|Value.of_ext Value.val_sort s|]
   | Cast (c, k, t) ->
-    ValBlk (5, [|
+    v_blk 5 [|
       Value.of_constr c;
       Value.of_ext Value.val_cast k;
       Value.of_constr t;
-    |])
+    |]
   | Prod (na, t, u) ->
-    ValBlk (6, [|
+    v_blk 6 [|
       of_name na;
       Value.of_constr t;
       Value.of_constr u;
-    |])
+    |]
   | Lambda (na, t, c) ->
-    ValBlk (7, [|
+    v_blk 7 [|
       of_name na;
       Value.of_constr t;
       Value.of_constr c;
-    |])
+    |]
   | LetIn (na, b, t, c) ->
-    ValBlk (8, [|
+    v_blk 8 [|
       of_name na;
       Value.of_constr b;
       Value.of_constr t;
       Value.of_constr c;
-    |])
+    |]
   | App (c, cl) ->
-    ValBlk (9, [|
+    v_blk 9 [|
       Value.of_constr c;
       Value.of_array Value.of_constr cl;
-    |])
+    |]
   | Const (cst, u) ->
-    ValBlk (10, [|
+    v_blk 10 [|
       Value.of_constant cst;
       of_instance u;
-    |])
+    |]
   | Ind (ind, u) ->
-    ValBlk (11, [|
+    v_blk 11 [|
       Value.of_ext Value.val_inductive ind;
       of_instance u;
-    |])
+    |]
   | Construct (cstr, u) ->
-    ValBlk (12, [|
+    v_blk 12 [|
       Value.of_ext Value.val_constructor cstr;
       of_instance u;
-    |])
+    |]
   | Case (ci, c, t, bl) ->
-    ValBlk (13, [|
+    v_blk 13 [|
       Value.of_ext Value.val_case ci;
       Value.of_constr c;
       Value.of_constr t;
       Value.of_array Value.of_constr bl;
-    |])
+    |]
   | Fix ((recs, i), def) ->
     let (nas, ts, cs) = of_rec_declaration def in
-    ValBlk (14, [|
+    v_blk 14 [|
       Value.of_array Value.of_int recs;
       Value.of_int i;
       nas;
       ts;
       cs;
-    |])
+    |]
   | CoFix (i, def) ->
     let (nas, ts, cs) = of_rec_declaration def in
-    ValBlk (15, [|
+    v_blk 15 [|
       Value.of_int i;
       nas;
       ts;
       cs;
-    |])
+    |]
   | Proj (p, c) ->
-    ValBlk (16, [|
+    v_blk 16 [|
       Value.of_ext Value.val_projection p;
       Value.of_constr c;
-    |])
+    |]
   end
 end
 
 let () = define1 "constr_make" valexpr begin fun knd ->
   let open Constr in
-  let c = match knd with
-  | ValBlk (0, [|n|]) ->
+  let c = match Tac2ffi.to_block knd with
+  | (0, [|n|]) ->
     let n = Value.to_int n in
     EConstr.mkRel n
-  | ValBlk (1, [|id|]) ->
+  | (1, [|id|]) ->
     let id = Value.to_ident id in
     EConstr.mkVar id
-  | ValBlk (2, [|n|]) ->
+  | (2, [|n|]) ->
     let n = Value.to_int n in
     EConstr.mkMeta n
-  | ValBlk (3, [|evk; args|]) ->
+  | (3, [|evk; args|]) ->
     let evk = Evar.unsafe_of_int (Value.to_int evk) in
     let args = Value.to_array Value.to_constr args in
     EConstr.mkEvar (evk, args)
-  | ValBlk (4, [|s|]) ->
+  | (4, [|s|]) ->
     let s = Value.to_ext Value.val_sort s in
     EConstr.mkSort (EConstr.Unsafe.to_sorts s)
-  | ValBlk (5, [|c; k; t|]) ->
+  | (5, [|c; k; t|]) ->
     let c = Value.to_constr c in
     let k = Value.to_ext Value.val_cast k in
     let t = Value.to_constr t in
     EConstr.mkCast (c, k, t)
-  | ValBlk (6, [|na; t; u|]) ->
+  | (6, [|na; t; u|]) ->
     let na = to_name na in
     let t = Value.to_constr t in
     let u = Value.to_constr u in
     EConstr.mkProd (na, t, u)
-  | ValBlk (7, [|na; t; c|]) ->
+  | (7, [|na; t; c|]) ->
     let na = to_name na in
     let t = Value.to_constr t in
     let u = Value.to_constr c in
     EConstr.mkLambda (na, t, u)
-  | ValBlk (8, [|na; b; t; c|]) ->
+  | (8, [|na; b; t; c|]) ->
     let na = to_name na in
     let b = Value.to_constr b in
     let t = Value.to_constr t in
     let c = Value.to_constr c in
     EConstr.mkLetIn (na, b, t, c)
-  | ValBlk (9, [|c; cl|]) ->
+  | (9, [|c; cl|]) ->
     let c = Value.to_constr c in
     let cl = Value.to_array Value.to_constr cl in
     EConstr.mkApp (c, cl)
-  | ValBlk (10, [|cst; u|]) ->
+  | (10, [|cst; u|]) ->
     let cst = Value.to_constant cst in
     let u = to_instance u in
     EConstr.mkConstU (cst, u)
-  | ValBlk (11, [|ind; u|]) ->
+  | (11, [|ind; u|]) ->
     let ind = Value.to_ext Value.val_inductive ind in
     let u = to_instance u in
     EConstr.mkIndU (ind, u)
-  | ValBlk (12, [|cstr; u|]) ->
+  | (12, [|cstr; u|]) ->
     let cstr = Value.to_ext Value.val_constructor cstr in
     let u = to_instance u in
     EConstr.mkConstructU (cstr, u)
-  | ValBlk (13, [|ci; c; t; bl|]) ->
+  | (13, [|ci; c; t; bl|]) ->
     let ci = Value.to_ext Value.val_case ci in
     let c = Value.to_constr c in
     let t = Value.to_constr t in
     let bl = Value.to_array Value.to_constr bl in
     EConstr.mkCase (ci, c, t, bl)
-  | ValBlk (14, [|recs; i; nas; ts; cs|]) ->
+  | (14, [|recs; i; nas; ts; cs|]) ->
     let recs = Value.to_array Value.to_int recs in
     let i = Value.to_int i in
     let def = to_rec_declaration (nas, ts, cs) in
     EConstr.mkFix ((recs, i), def)
-  | ValBlk (15, [|i; nas; ts; cs|]) ->
+  | (15, [|i; nas; ts; cs|]) ->
     let i = Value.to_int i in
     let def = to_rec_declaration (nas, ts, cs) in
     EConstr.mkCoFix (i, def)
-  | ValBlk (16, [|p; c|]) ->
+  | (16, [|p; c|]) ->
     let p = Value.to_ext Value.val_projection p in
     let c = Value.to_constr c in
     EConstr.mkProj (p, c)
@@ -622,8 +623,8 @@ let () = define1 "case" closure begin fun f ->
       set_bt info >>= fun info ->
       k (e, info)
     end in
-    return (ValBlk (0, [| Value.of_tuple [| x; Value.of_closure k |] |]))
-  | Proofview.Fail e -> return (ValBlk (1, [| Value.of_exn e |]))
+    return (v_blk 0 [| Value.of_tuple [| x; Value.of_closure k |] |])
+  | Proofview.Fail e -> return (v_blk 1 [| Value.of_exn e |])
   end
 end
 
@@ -791,7 +792,7 @@ let interp_constr flags ist c =
   pf_apply begin fun env sigma ->
   try
     let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in
-    let c = ValExt (Value.val_constr, c) in
+    let c = Value.of_constr c in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT c
   with e when catchable_exception e ->
@@ -827,7 +828,7 @@ let () =
   define_ml_object Tac2quote.wit_open_constr obj
 
 let () =
-  let interp _ id = return (ValExt (Value.val_ident, id)) in
+  let interp _ id = return (Value.of_ident id) in
   let print _ id = str "ident:(" ++ Id.print id ++ str ")" in
   let obj = {
     ml_intern = (fun _ _ id -> GlbVal id, gtypref t_ident);
@@ -843,7 +844,7 @@ let () =
     GlbVal pat, gtypref t_pattern
   in
   let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in
-  let interp _ c = return (ValExt (Value.val_pattern, c)) in
+  let interp _ c = return (Value.of_pattern c) in
   let obj = {
     ml_intern = intern;
     ml_interp = interp;
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 24db19d02a..cd4b701ca7 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -774,7 +774,7 @@ let pr_frame = function
 let () = register_handler begin function
 | Tac2interp.LtacError (kn, args) ->
   let t_exn = KerName.make2 Tac2env.coq_prefix (Label.make "exn") in
-  let v = Tac2ffi.ValOpn (kn, args) in
+  let v = Tac2ffi.of_open (kn, args) in
   let t = GTypRef (Other t_exn, []) in
   let c = Tac2print.pr_valexpr (Global.env ()) Evd.empty v t in
   hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 5460643bb5..7960d4d45f 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -41,6 +41,35 @@ type 'a arity = (valexpr, 'a) arity0
 
 let mk_closure arity f = MLTactic (arity, f)
 
+module Valexpr =
+struct
+
+type t = valexpr
+
+let is_int = function
+| ValInt _ -> true
+| ValBlk _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ -> false
+
+let tag v = match v with
+| ValBlk (n, _) -> n
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+  CErrors.anomaly (Pp.str "Unexpected value shape")
+
+let field v n = match v with
+| ValBlk (_, v) -> v.(n)
+| ValInt _ | ValStr _ | ValCls _ | ValOpn _ | ValExt _ ->
+  CErrors.anomaly (Pp.str "Unexpected value shape")
+
+let set_field v n w = match v with
+| ValBlk (_, v) -> v.(n) <- w
+| ValInt _ | 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
+
+end
+
 type 'a repr = {
   r_of : 'a -> valexpr;
   r_to : valexpr -> 'a;
@@ -251,9 +280,26 @@ let array r = {
   r_id = false;
 }
 
+let of_block (n, args) = ValBlk (n, args)
+let to_block = function
+| ValBlk (n, args) -> (n, args)
+| _ -> assert false
+
 let block = {
-  r_of = of_tuple;
-  r_to = to_tuple;
+  r_of = of_block;
+  r_to = to_block;
+  r_id = false;
+}
+
+let of_open (kn, args) = ValOpn (kn, args)
+
+let to_open = function
+| ValOpn (kn, args) -> (kn, args)
+| _ -> assert false
+
+let open_ = {
+  r_of = of_open;
+  r_to = to_open;
   r_id = false;
 }
 
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index af854e2d07..36743f3346 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -36,6 +36,17 @@ val arity_suc : 'a arity -> (valexpr -> 'a) arity
 
 val mk_closure : 'v arity -> 'v -> closure
 
+module Valexpr :
+sig
+  type t = valexpr
+  val is_int : t -> bool
+  val tag : t -> int
+  val field : t -> int -> t
+  val set_field : t -> int -> t -> unit
+  val make_block : int -> t array -> t
+  val make_int : int -> t
+end
+
 (** {5 Ltac2 FFI} *)
 
 type 'a repr = {
@@ -89,7 +100,9 @@ val of_closure : closure -> valexpr
 val to_closure : valexpr -> closure
 val closure : closure repr
 
-val block : valexpr array repr
+val of_block : (int * valexpr array) -> valexpr
+val to_block : valexpr -> (int * valexpr array)
+val block : (int * valexpr array) repr
 
 val of_array : ('a -> valexpr) -> 'a array -> valexpr
 val to_array : (valexpr -> 'a) -> valexpr -> 'a array
@@ -122,6 +135,10 @@ 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 of_open : KerName.t * valexpr array -> valexpr
+val to_open : valexpr -> KerName.t * valexpr array
+val open_ : (KerName.t * valexpr array) repr
+
 type ('a, 'b) fun1
 
 val app_fun1 : ('a, 'b) fun1 -> 'a repr -> 'b repr -> 'a -> 'b Proofview.tactic
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 58a3a9a4ec..db30f52772 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -80,8 +80,8 @@ let get_ref ist kn =
 let return = Proofview.tclUNIT
 
 let rec interp (ist : environment) = function
-| GTacAtm (AtmInt n) -> return (ValInt n)
-| GTacAtm (AtmStr s) -> return (ValStr (Bytes.of_string s))
+| GTacAtm (AtmInt n) -> return (Tac2ffi.of_int n)
+| GTacAtm (AtmStr s) -> return (Tac2ffi.of_string (Bytes.of_string s))
 | GTacVar id -> return (get_var ist id)
 | GTacRef kn ->
   let data = get_ref ist kn in
@@ -89,7 +89,7 @@ let rec interp (ist : environment) = function
 | GTacFun (ids, e) ->
   let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
   let f = interp_app cls in
-  return (ValCls f)
+  return (Tac2ffi.of_closure f)
 | GTacApp (f, args) ->
   interp ist f >>= fun f ->
   Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args ->
@@ -105,7 +105,7 @@ let rec interp (ist : environment) = function
   let map (na, e) = match e with
   | GTacFun (ids, e) ->
     let cls = { clos_ref = None; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
-    let f = ValCls (interp_app cls) in
+    let f = Tac2ffi.of_closure (interp_app cls) in
     na, cls, f
   | _ -> anomaly (str "Ill-formed recursive function")
   in
@@ -119,10 +119,10 @@ let rec interp (ist : environment) = function
   let iter (_, e, _) = e.clos_env <- ist.env_ist in
   let () = List.iter iter fixs in
   interp ist e
-| GTacCst (_, n, []) -> return (ValInt n)
+| GTacCst (_, n, []) -> return (Valexpr.make_int n)
 | GTacCst (_, n, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
-  return (ValBlk (n, Array.of_list el))
+  return (Valexpr.make_block n (Array.of_list el))
 | GTacCse (e, _, cse0, cse1) ->
   interp ist e >>= fun e -> interp_case ist e cse0 cse1
 | GTacWth { opn_match = e; opn_branch = cse; opn_default = def } ->
@@ -135,7 +135,7 @@ let rec interp (ist : environment) = function
   interp_set ist e p r
 | GTacOpn (kn, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
-  return (ValOpn (kn, Array.of_list el))
+  return (Tac2ffi.of_open (kn, Array.of_list el))
 | GTacPrm (ml, el) ->
   Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
   with_frame (FrPrim ml) (Tac2ffi.apply (Tac2env.interp_primitive ml) el)
@@ -156,17 +156,17 @@ and interp_app f =
   in
   Tac2ffi.abstract (List.length f.clos_var) ans
 
-and interp_case ist e cse0 cse1 = match e with
-| ValInt n -> interp ist cse0.(n)
-| ValBlk (n, args) ->
-  let (ids, e) = cse1.(n) in
-  let ist = CArray.fold_left2 push_name ist ids args in
-  interp ist e
-| ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
-  anomaly (str "Unexpected value shape")
+and interp_case ist e cse0 cse1 =
+  if Valexpr.is_int e then
+    interp ist cse0.(Tac2ffi.to_int e)
+  else
+    let (n, args) = Tac2ffi.to_block e in
+    let (ids, e) = cse1.(n) in
+    let ist = CArray.fold_left2 push_name ist ids args in
+    interp ist e
 
-and interp_with ist e cse def = match e with
-| ValOpn (kn, args) ->
+and interp_with ist e cse def = 
+  let (kn, args) = Tac2ffi.to_open e in
   let br = try Some (KNmap.find kn cse) with Not_found -> None in
   begin match br with
   | None ->
@@ -178,24 +178,16 @@ and interp_with ist e cse def = match e with
     let ist = CArray.fold_left2 push_name ist ids args in
     interp ist p
   end
-| ValInt _ | ValBlk _ | ValExt _ | ValStr _ | ValCls _ ->
-  anomaly (str "Unexpected value shape")
-
-and interp_proj ist e p = match e with
-| ValBlk (_, args) ->
-  return args.(p)
-| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
-  anomaly (str "Unexpected value shape")
-
-and interp_set ist e p r = match e with
-| ValBlk (_, args) ->
-  let () = args.(p) <- r in
-  return (ValInt 0)
-| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
-  anomaly (str "Unexpected value shape")
+
+and interp_proj ist e p =
+  return (Valexpr.field e p)
+
+and interp_set ist e p r =
+  let () = Valexpr.set_field e p r in
+  return (Valexpr.make_int 0)
 
 and eval_pure kn = function
-| GTacAtm (AtmInt n) -> ValInt n
+| GTacAtm (AtmInt n) -> Valexpr.make_int n
 | GTacRef kn ->
   let { Tac2env.gdata_expr = e } =
     try Tac2env.interp_global kn
@@ -205,10 +197,10 @@ and eval_pure kn = function
 | GTacFun (na, e) ->
   let cls = { clos_ref = kn; clos_env = Id.Map.empty; clos_var = na; clos_exp = e } in
   let f = interp_app cls in
-  ValCls f
-| GTacCst (_, n, []) -> ValInt n
-| GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_unnamed el)
-| GTacOpn (kn, el) -> ValOpn (kn, Array.map_of_list eval_unnamed el)
+  Tac2ffi.of_closure f
+| GTacCst (_, n, []) -> Valexpr.make_int n
+| GTacCst (_, n, el) -> Valexpr.make_block n (Array.map_of_list eval_unnamed el)
+| GTacOpn (kn, el) -> Tac2ffi.of_open (kn, Array.map_of_list eval_unnamed el)
 | GTacAtm (AtmStr _) | GTacLet _ | GTacVar _ | GTacSet _
 | GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ ->
   anomaly (Pp.str "Term is not a syntactical value")
diff --git a/src/tac2print.ml b/src/tac2print.ml
index d39051c93e..45360a61f4 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -381,29 +381,27 @@ let rec pr_valexpr env sigma v t = match kind t with
       (** Shouldn't happen thanks to kind *)
       assert false
     | GTydAlg alg ->
-      begin match v with
-      | ValInt n -> pr_internal_constructor kn n true
-      | ValBlk (n, args) ->
+      if Valexpr.is_int v then
+        pr_internal_constructor kn (Tac2ffi.to_int v) true
+      else
+        let (n, args) = Tac2ffi.to_block v in
         let (id, tpe) = find_constructor n false alg.galg_constructors in
         let knc = change_kn_label kn id in
         let args = pr_constrargs env sigma params args tpe in
         hv 2 (pr_constructor knc ++ spc () ++ str "(" ++ args ++ str ")")
-      | _ -> str "<unknown>"
-      end
     | GTydRec rcd -> str "{}"
     | GTydOpn ->
-      begin match v with
-      | ValOpn (knc, [||]) -> pr_constructor knc
-      | ValOpn (knc, args) ->
+      begin match Tac2ffi.to_open v with
+      | (knc, [||]) -> pr_constructor knc
+      | (knc, args) ->
         let data = Tac2env.interp_constructor knc in
         let args = pr_constrargs env sigma params args data.Tac2env.cdata_args in
         hv 2 (pr_constructor knc ++ spc () ++ str "(" ++ args ++ str ")")
-      | _ -> str "<unknown>"
       end
   end
 | GTypArrow _ -> str "<fun>"
 | GTypRef (Tuple _, tl) ->
-  let blk = Array.to_list (block.r_to v) in
+  let blk = Array.to_list (snd (block.r_to v)) in
   if List.length blk == List.length tl then
     let prs = List.map2 (fun v t -> pr_valexpr env sigma v t) blk tl in
     hv 2 (str "(" ++ prlist_with_sep pr_comma (fun p -> p) prs ++ str ")")
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 5f61081a76..0e0eb116b3 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -22,17 +22,17 @@ let return x = Proofview.tclUNIT x
 let v_unit = Value.of_unit ()
 let thaw f = Tac2ffi.apply (Value.to_closure f) [v_unit]
 
-let to_pair f g = function
-| ValBlk (0, [| x; y |]) -> (f x, g y)
+let to_pair f g v = match Value.to_tuple v with
+| [| x; y |] -> (f x, g y)
 | _ -> assert false
 
 let to_name c = match Value.to_option Value.to_ident c with
 | None -> Anonymous
 | Some id -> Name id
 
-let to_qhyp = function
-| ValBlk (0, [| i |]) -> AnonHyp (Value.to_int i)
-| ValBlk (1, [| id |]) -> NamedHyp (Value.to_ident id)
+let to_qhyp v = match Value.to_block v with
+| (0, [| i |]) -> AnonHyp (Value.to_int i)
+| (1, [| id |]) -> NamedHyp (Value.to_ident id)
 | _ -> assert false
 
 let to_bindings = function
@@ -43,8 +43,8 @@ let to_bindings = function
   ExplicitBindings ((Value.to_list (fun p -> to_pair to_qhyp Value.to_constr p) vl))
 | _ -> assert false
 
-let to_constr_with_bindings = function
-| ValBlk (0, [| c; bnd |]) -> (Value.to_constr c, to_bindings bnd)
+let to_constr_with_bindings v = match Value.to_tuple v with
+| [| c; bnd |] -> (Value.to_constr c, to_bindings bnd)
 | _ -> assert false
 
 let to_int_or_var i = ArgArg (Value.to_int i)
@@ -56,16 +56,16 @@ let to_occurrences f = function
 | ValBlk (1, [| vl |]) -> OnlyOccurrences (Value.to_list f vl)
 | _ -> assert false
 
-let to_hyp_location_flag = function
-| ValInt 0 -> InHyp
-| ValInt 1 -> InHypTypeOnly
-| ValInt 2 -> InHypValueOnly
+let to_hyp_location_flag v = match Value.to_int v with
+| 0 -> InHyp
+| 1 -> InHypTypeOnly
+| 2 -> InHypValueOnly
 | _ -> assert false
 
-let to_clause = function
-| ValBlk (0, [| hyps; concl |]) ->
-  let cast = function
-  | ValBlk (0, [| hyp; occ; flag |]) ->
+let to_clause v = match Value.to_tuple v with
+| [| hyps; concl |] ->
+  let cast v = match Value.to_tuple v with
+  | [| hyp; occ; flag |] ->
     ((to_occurrences to_int_or_var occ, Value.to_ident hyp), to_hyp_location_flag flag)
   | _ -> assert false
   in
@@ -73,8 +73,8 @@ let to_clause = function
   { onhyps = hyps; concl_occs = to_occurrences to_int_or_var concl; }
 | _ -> assert false
 
-let to_red_flag = function
-| ValBlk (0, [| beta; iota; fix; cofix; zeta; delta; const |]) ->
+let to_red_flag v = match Value.to_tuple v with
+| [| beta; iota; fix; cofix; zeta; delta; const |] ->
   {
     rBeta = Value.to_bool beta;
     rMatch = Value.to_bool iota;
@@ -92,10 +92,10 @@ let to_pattern_with_occs pat =
 let to_constr_with_occs c =
   to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) c
 
-let rec to_intro_pattern = function
-| ValBlk (0, [| b |]) -> IntroForthcoming (Value.to_bool b)
-| ValBlk (1, [| pat |]) -> IntroNaming (to_intro_pattern_naming pat)
-| ValBlk (2, [| act |]) -> IntroAction (to_intro_pattern_action act)
+let rec to_intro_pattern v = match Value.to_block v with
+| (0, [| b |]) -> IntroForthcoming (Value.to_bool b)
+| (1, [| pat |]) -> IntroNaming (to_intro_pattern_naming pat)
+| (2, [| act |]) -> IntroAction (to_intro_pattern_action act)
 | _ -> assert false
 
 and to_intro_pattern_naming = function
@@ -116,26 +116,26 @@ and to_intro_pattern_action = function
 | ValBlk (3, [| b |]) -> IntroRewrite (Value.to_bool b)
 | _ -> assert false
 
-and to_or_and_intro_pattern = function
-| ValBlk (0, [| ill |]) ->
+and to_or_and_intro_pattern v = match Value.to_block v with
+| (0, [| ill |]) ->
   IntroOrPattern (Value.to_list to_intro_patterns ill)
-| ValBlk (1, [| il |]) ->
+| (1, [| il |]) ->
   IntroAndPattern (to_intro_patterns il)
 | _ -> assert false
 
 and to_intro_patterns il =
   Value.to_list to_intro_pattern il
 
-let to_destruction_arg = function
-| ValBlk (0, [| c |]) ->
+let to_destruction_arg v = match Value.to_block v with
+| (0, [| c |]) ->
   let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
   ElimOnConstr c
-| ValBlk (1, [| id |]) -> ElimOnIdent (Value.to_ident id)
-| ValBlk (2, [| n |]) -> ElimOnAnonHyp (Value.to_int n)
+| (1, [| id |]) -> ElimOnIdent (Value.to_ident id)
+| (2, [| n |]) -> ElimOnAnonHyp (Value.to_int n)
 | _ -> assert false
 
-let to_induction_clause = function
-| ValBlk (0, [| arg; eqn; as_; in_ |]) ->
+let to_induction_clause v = match Value.to_tuple v with
+| [| arg; eqn; as_; in_ |] ->
   let arg = to_destruction_arg arg in
   let eqn = Value.to_option to_intro_pattern_naming eqn in
   let as_ = Value.to_option to_or_and_intro_pattern as_ in
@@ -144,14 +144,14 @@ let to_induction_clause = function
 | _ ->
   assert false
 
-let to_assertion = function
-| ValBlk (0, [| ipat; t; tac |]) ->
+let to_assertion v = match Value.to_block v with
+| (0, [| ipat; t; tac |]) ->
   let to_tac t = Proofview.tclIGNORE (thaw t) in
   let ipat = Value.to_option to_intro_pattern ipat in
   let t = Value.to_constr t in
   let tac = Value.to_option to_tac tac in
   AssertType (ipat, t, tac)
-| ValBlk (1, [| id; c |]) ->
+| (1, [| id; c |]) ->
   AssertValue (Value.to_ident id, Value.to_constr c)
 | _ -> assert false
 
@@ -162,30 +162,29 @@ let to_multi = function
 | ValInt 1 -> RepeatPlus
 | _ -> assert false
 
-let to_rewriting = function
-| ValBlk (0, [| orient; repeat; c |]) ->
+let to_rewriting v = match Value.to_tuple v with
+| [| orient; repeat; c |] ->
   let orient = Value.to_option Value.to_bool orient in
   let repeat = to_multi repeat in
-  (** FIXME: lost backtrace *)
   let c = thaw c >>= fun c -> return (to_constr_with_bindings c) in
   (orient, repeat, c)
 | _ -> assert false
 
-let to_debug = function
-| ValInt 0 -> Hints.Off
-| ValInt 1 -> Hints.Info
-| ValInt 2 -> Hints.Debug
+let to_debug v = match Value.to_int v with
+| 0 -> Hints.Off
+| 1 -> Hints.Info
+| 2 -> Hints.Debug
 | _ -> assert false
 
-let to_strategy = function
-| ValInt 0 -> Class_tactics.Bfs
-| ValInt 1 -> Class_tactics.Dfs
+let to_strategy v = match Value.to_int v with
+| 0 -> Class_tactics.Bfs
+| 1 -> Class_tactics.Dfs
 | _ -> assert false
 
-let to_inversion_kind = function
-| ValInt 0 -> Misctypes.SimpleInversion
-| ValInt 1 -> Misctypes.FullInversion
-| ValInt 2 -> Misctypes.FullInversionClear
+let to_inversion_kind v = match Value.to_int v with
+| 0 -> Misctypes.SimpleInversion
+| 1 -> Misctypes.FullInversion
+| 2 -> Misctypes.FullInversionClear
 | _ -> assert false
 
 let to_move_location = function
@@ -258,8 +257,8 @@ let () = define_prim2 "tac_case" begin fun ev c ->
 end
 
 let () = define_prim1 "tac_generalize" begin fun cl ->
-  let cast = function
-  | ValBlk (0, [| c; occs; na |]) ->
+  let cast v = match Value.to_tuple v with
+  | [| c; occs; na |] ->
     ((to_occurrences Value.to_int occs, Value.to_constr c), to_name na)
   | _ -> assert false
   in