Simplifying the code of Tacinterp.

1 files changed, 7 insertions, 14 deletions

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index b9d074a3d..6e76b1910 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1546,28 +1546,21 @@ and interp_genarg ist x : Val.t Ftactic.t =
     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
+      let map x = interp_genarg ist (Genarg.in_gen (glbwit wit) x) in
       Ftactic.List.map map x >>= fun l ->
-      Ftactic.return (Value.of_list (val_tag wit) l)
+      Ftactic.return (Val.Dyn (Val.list_tag, l))
     | OptArg wit ->
-      let ans = match x with
-      | None -> Ftactic.return (Value.of_option (val_tag wit) None)
+      begin match x with
+      | None -> Ftactic.return (Val.Dyn (Val.opt_tag, 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
-      ans
+        Ftactic.return (Val.Dyn (Val.opt_tag, Some x))
+      end
     | 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 (Value.of_pair (val_tag wit1) (val_tag wit2) (p, q))
+      Ftactic.return (Val.Dyn (Val.pair_tag, (p, q)))
     | ExtraArg s ->
       Geninterp.interp wit ist x >>= fun x ->
       Ftactic.return (in_gen (Topwit wit) x)