Getting rid of the awkward unpack mechanism from Genarg.

1 files changed, 17 insertions, 23 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6f6c4a05a..14e0fed31 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -718,35 +718,29 @@ and intern_match_rule onlytac ist = function
       Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
   | [] -> []
 
-and intern_genarg ist x =
-  match genarg_tag x with
-  | ListArgType _ ->
-      let list_unpacker wit l =
-        let map x =
-          let ans = intern_genarg ist (in_gen (rawwit wit) x) in
-          out_gen (glbwit wit) ans
-        in
-        in_gen (glbwit (wit_list wit)) (List.map map (raw l))
+and intern_genarg ist (GenArg (Rawwit wit, x)) =
+  match wit with
+  | ListArg wit ->
+      let map x =
+        let ans = intern_genarg ist (in_gen (rawwit wit) x) in
+        out_gen (glbwit wit) ans
       in
-      list_unpack { list_unpacker } x
-  | OptArgType _ ->
-      let opt_unpacker wit o = match raw o with
+      in_gen (glbwit (wit_list wit)) (List.map map x)
+  | OptArg wit ->
+      let ans = match x with
       | None -> in_gen (glbwit (wit_opt wit)) None
       | Some x ->
         let s = out_gen (glbwit wit) (intern_genarg ist (in_gen (rawwit wit) x)) in
         in_gen (glbwit (wit_opt wit)) (Some s)
       in
-      opt_unpack { opt_unpacker } x
-  | PairArgType _ ->
-      let pair_unpacker wit1 wit2 o =
-        let p, q = raw o in
-        let p = out_gen (glbwit wit1) (intern_genarg ist (in_gen (rawwit wit1) p)) in
-        let q = out_gen (glbwit wit2) (intern_genarg ist (in_gen (rawwit wit2) q)) in
-        in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
-      in
-      pair_unpack { pair_unpacker } x
-  | ExtraArgType s ->
-      snd (Genintern.generic_intern ist x)
+      ans
+  | PairArg (wit1, wit2) ->
+      let p, q = x in
+      let p = out_gen (glbwit wit1) (intern_genarg ist (in_gen (rawwit wit1) p)) in
+      let q = out_gen (glbwit wit2) (intern_genarg ist (in_gen (rawwit wit2) q)) in
+      in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
+  | ExtraArg s ->
+      snd (Genintern.generic_intern ist (in_gen (rawwit wit) x))
 
 (** Other entry points *)