From d3ee6b2fbcd0fbb666af7f1920446e809e8d6e1e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 17 Jan 2016 01:58:05 +0100
Subject: Getting rid of the awkward unpack mechanism from Genarg.

---
 tactics/geninterp.ml |  9 +++------
 tactics/tacintern.ml | 40 +++++++++++++++++-----------------------
 tactics/tacinterp.ml | 46 +++++++++++++++++++++-------------------------
 tactics/tacsubst.ml  | 40 +++++++++++++++++-----------------------
 4 files changed, 58 insertions(+), 77 deletions(-)

(limited to 'tactics')

diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
index dff87d3a82..fd4f7315e3 100644
--- a/tactics/geninterp.ml
+++ b/tactics/geninterp.ml
@@ -29,10 +29,7 @@ module Interp = Register(InterpObj)
 let interp = Interp.obj
 let register_interp0 = Interp.register0
 
-let generic_interp ist v =
+let generic_interp ist (GenArg (Glbwit wit, v)) =
   let open Ftactic.Notations in
-  let unpacker wit v =
-    interp wit ist (glb v) >>= fun ans ->
-    Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
-  in
-  unpack { unpacker; } v
+  interp wit ist v >>= fun ans ->
+  Ftactic.return (Val.Dyn (val_tag (topwit wit), ans))
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6f6c4a05a1..14e0fed31d 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 *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71a6e043b5..8a16ed3899 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1524,38 +1524,34 @@ and interp_genarg ist x : Val.t Ftactic.t =
       interp_genarg_var_list ist x
     else if argument_type_eq tag (unquote (topwit (wit_list wit_constr))) then
       interp_genarg_constr_list ist x
-    else match tag with
-    | ListArgType _ ->
-      let list_unpacker wit l =
-        let map x =
-          interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
-          Ftactic.return (Value.cast (topwit wit) x)
-        in
-        Ftactic.List.map map (glb l) >>= fun l ->
-        Ftactic.return (Value.of_list (val_tag wit) l)
+    else
+    let GenArg (Glbwit wit, x) = x in
+    match wit with
+    | ListArg wit ->
+      let map x =
+        interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
+        Ftactic.return (Value.cast (topwit wit) x)
       in
-      list_unpack { list_unpacker } x
-    | OptArgType _ ->
-      let opt_unpacker wit o = match glb o with
+      Ftactic.List.map map x >>= fun l ->
+      Ftactic.return (Value.of_list (val_tag wit) l)
+    | OptArg wit ->
+      let ans = match x with
       | None -> Ftactic.return (Value.of_option (val_tag wit) None)
       | Some x ->
         interp_genarg ist (Genarg.in_gen (glbwit wit) x) >>= fun x ->
         let x = Value.cast (topwit wit) x in
         Ftactic.return (Value.of_option (val_tag wit) (Some x))
       in
-      opt_unpack { opt_unpacker } x
-    | PairArgType _ ->
-      let pair_unpacker wit1 wit2 o =
-        let (p, q) = glb o in
-        interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p ->
-        interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q ->
-        let p = Value.cast (topwit wit1) p in
-        let q = Value.cast (topwit wit2) q in
-        Ftactic.return (Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q)))
-      in
-      pair_unpack { pair_unpacker } x
-    | ExtraArgType _ ->
-      Geninterp.generic_interp ist x
+      ans
+    | PairArg (wit1, wit2) ->
+      let (p, q) = x in
+      interp_genarg ist (Genarg.in_gen (glbwit wit1) p) >>= fun p ->
+      interp_genarg ist (Genarg.in_gen (glbwit wit2) q) >>= fun q ->
+      let p = Value.cast (topwit wit1) p in
+      let q = Value.cast (topwit wit2) q in
+      Ftactic.return (Val.Dyn (Val.Pair (val_tag wit1, val_tag wit2), (p, q)))
+    | ExtraArg s ->
+      Geninterp.generic_interp ist (Genarg.in_gen (glbwit wit) x)
 
 (** returns [true] for genargs which have the same meaning
     independently of goals. *)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 4f79115240..c74f6093a2 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -274,35 +274,29 @@ and subst_match_rule subst = function
       ::(subst_match_rule subst tl)
   | [] -> []
 
-and subst_genarg subst (x:glob_generic_argument) =
-  match genarg_tag x with
-  | ListArgType _ ->
-    let list_unpacker wit l =
-      let map x =
-        let ans = subst_genarg subst (in_gen (glbwit wit) x) in
-        out_gen (glbwit wit) ans
-      in
-      in_gen (glbwit (wit_list wit)) (List.map map (glb l))
+and subst_genarg subst (GenArg (Glbwit wit, x)) =
+  match wit with
+  | ListArg wit ->
+    let map x =
+      let ans = subst_genarg subst (in_gen (glbwit wit) x) in
+      out_gen (glbwit wit) ans
     in
-    list_unpack { list_unpacker } x
-  | OptArgType _ ->
-    let opt_unpacker wit o = match glb 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) (subst_genarg subst (in_gen (glbwit 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 = glb o in
-        let p = out_gen (glbwit wit1) (subst_genarg subst (in_gen (glbwit wit1) p)) in
-        let q = out_gen (glbwit wit2) (subst_genarg subst (in_gen (glbwit wit2) q)) in
-        in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
-      in
-      pair_unpack { pair_unpacker } x
-  | ExtraArgType s ->
-      Genintern.generic_substitute subst x
+    ans
+  | PairArg (wit1, wit2) ->
+    let p, q = x in
+    let p = out_gen (glbwit wit1) (subst_genarg subst (in_gen (glbwit wit1) p)) in
+    let q = out_gen (glbwit wit2) (subst_genarg subst (in_gen (glbwit wit2) q)) in
+    in_gen (glbwit (wit_pair wit1 wit2)) (p, q)
+  | ExtraArg s ->
+      Genintern.generic_substitute subst (in_gen (glbwit wit) x)
 
 (** Registering *)
 
-- 
cgit v1.2.3