Simplification of Genarg unpackers.

Instead of having a version of unpackers for each level, we use a dummy argument
to force unification of types.

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
index 4a49ae287f..5d76686bb8 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