5 files changed, 25 insertions, 29 deletions
diff --git a/interp/genintern.ml b/interp/genintern.ml
index a8f82d998..b066ca529 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -39,11 +39,11 @@ let intern = Intern.obj
 let register_intern0 = Intern.register0
 
 let generic_intern ist v =
-  let unpack wit v =
-    let (ist, v) = intern wit ist v in
+  let unpacker wit v =
+    let (ist, v) = intern wit ist (raw v) in
     (ist, in_gen (glbwit wit) v)
   in
-  raw_unpack { raw_unpack = unpack; } v
+  unpack { unpacker; } v
 
 (** Substitution functions *)
 
@@ -51,7 +51,7 @@ let substitute = Subst.obj
 let register_subst0 = Subst.register0
 
 let generic_substitute subs v =
-  let unpack wit v = in_gen (glbwit wit) (substitute wit subs v) in
-  glb_unpack { glb_unpack = unpack; } v
+  let unpacker wit v = in_gen (glbwit wit) (substitute wit subs (glb v)) in
+  unpack { unpacker; } v
 
 let () = Hook.set Detyping.subst_genarg_hook generic_substitute
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 89b6f23de..b85fef087 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -159,18 +159,16 @@ type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
-type 'r raw_unpack =
-  { raw_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'a -> 'r }
+type ('a, 'b, 'c, 'l) cast = Obj.t
 
-type 'r glb_unpack =
-  { glb_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'b -> 'r }
+let raw = Obj.obj
+let glb = Obj.obj
+let top = Obj.obj
 
-type 'r top_unpack =
-  { top_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'c -> 'r }
+type ('r, 'l) unpacker =
+  { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
 
-let raw_unpack pack (t, obj) = pack.raw_unpack t (Obj.obj obj)
-let glb_unpack pack (t, obj) = pack.glb_unpack t (Obj.obj obj)
-let top_unpack pack (t, obj) = pack.top_unpack t (Obj.obj obj)
+let unpack pack (t, obj) = pack.unpacker t (Obj.obj obj)
 
 (** Creating args *)
 
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 45f0dddf2..e96f21c10 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -143,18 +143,16 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
 
 (** {6 Destructors} *)
 
-type 'r raw_unpack =
-  { raw_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'a -> 'r }
+type ('a, 'b, 'c, 'l) cast
 
-type 'r glb_unpack =
-  { glb_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'b -> 'r }
+val raw : ('a, 'b, 'c, rlevel) cast -> 'a
+val glb : ('a, 'b, 'c, glevel) cast -> 'b
+val top : ('a, 'b, 'c, tlevel) cast -> 'c
 
-type 'r top_unpack =
-  { top_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'c -> 'r }
+type ('r, 'l) unpacker =
+  { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
 
-val raw_unpack : 'r raw_unpack -> rlevel generic_argument -> 'r
-val glb_unpack : 'r glb_unpack -> glevel generic_argument -> 'r
-val top_unpack : 'r top_unpack -> tlevel generic_argument -> 'r
+val unpack : ('r, 'l) unpacker -> 'l generic_argument -> 'r
 (** Existential-type destructors. *)
 
 (** {6 Manipulation of generic arguments}
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 02f2dd63b..f8458ad6e 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -40,6 +40,6 @@ let raw_print wit v = (Print.obj wit).raw v
 let glb_print wit v = (Print.obj wit).glb v
 let top_print wit v = (Print.obj wit).top v
 
-let generic_raw_print v = raw_unpack { raw_unpack = raw_print; } v
-let generic_glb_print v = glb_unpack { glb_unpack = glb_print; } v
-let generic_top_print v = top_unpack { top_unpack = top_print; } v
+let generic_raw_print v = unpack { unpacker = fun w v -> raw_print w (raw v); } v
+let generic_glb_print v = unpack { unpacker = fun w v -> glb_print w (glb v); } v
+let generic_top_print v = unpack { unpacker = fun w v -> top_print w (top v); } v
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
index 4a49ae287..5d76686bb 100644
--- a/tactics/geninterp.ml
+++ b/tactics/geninterp.ml
@@ -31,8 +31,8 @@ let interp = Interp.obj
 let register_interp0 = Interp.register0
 
 let generic_interp ist gl v =
-  let unpack wit v =
-    let (sigma, ans) = interp wit ist gl v in
+  let unpacker wit v =
+    let (sigma, ans) = interp wit ist gl (glb v) in
     (sigma, in_gen (topwit wit) ans)
   in
-  glb_unpack { glb_unpack = unpack; } v
+  unpack { unpacker; } v