Moving val_cast to Tacinterp.

3 files changed, 42 insertions, 51 deletions

diff --git a/lib/genarg.ml b/lib/genarg.ml
index 58d83ce7a..37b31a511 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -285,50 +285,7 @@ let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
 | ExtraArg s ->
   match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn
 
-exception CastError of argument_type * Val.t
-
-let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
-  let Val.Dyn (t', x) = v in
-  match Val.eq t t' with
-  | None -> None
-  | Some Refl -> Some x
-
-let try_prj wit v = match prj (val_tag wit) v with
-| None -> raise (CastError (untype wit, v))
-| Some x -> x
-
-let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c =
-fun wit v -> match wit with
-| ExtraArg _ -> try_prj wit v
-| ListArg t ->
-  let Val.Dyn (tag, v) = v in
-  begin match tag with
-  | Val.List tag ->
-    let map x = val_cast t (Val.Dyn (tag, x)) in
-    List.map map v
-  | _ -> raise (CastError (untype wit, Val.Dyn (tag, v)))
-  end
-| OptArg t ->
-  let Val.Dyn (tag, v) = v in
-  begin match tag with
-  | Val.Opt tag ->
-    let map x = val_cast t (Val.Dyn (tag, x)) in
-    Option.map map v
-  | _ ->  raise (CastError (untype wit, Val.Dyn (tag, v)))
-  end
-| PairArg (t1, t2) ->
-  let Val.Dyn (tag, v) = v in
-  begin match tag with
-  | Val.Pair (tag1, tag2) ->
-    let (v1, v2) = v in
-    let v1 = Val.Dyn (tag1, v1) in
-    let v2 = Val.Dyn (tag2, v2) in
-    (val_cast t1 v1, val_cast t2 v2)
-  | _ ->  raise (CastError (untype wit, Val.Dyn (tag, v)))
-  end
-
 let val_tag = function Topwit t -> val_tag t
-let val_cast = function Topwit t -> val_cast t
 
 (** Registering genarg-manipulating functions *)
 
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 8d1a43982..024c7a456 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -185,8 +185,6 @@ val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag
 (** Retrieve the dynamic type associated to a toplevel genarg. Only works for
     ground generic arguments. *)
 
-val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a
-
 (** {6 Type reification} *)
 
 type argument_type =
@@ -196,9 +194,6 @@ type argument_type =
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
-exception CastError of argument_type * Val.t
-(** Exception raised by {!val_cast} *)
-
 (** {6 Equalities} *)
 
 val argument_type_eq : argument_type -> argument_type -> bool
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8a16ed389..8db91c07f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -149,10 +149,49 @@ module Value = struct
     let Val.Dyn (tag, _) = v in
     let tag = Val.repr tag in
     errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag
-      ++ str " while type " ++ Genarg.pr_argument_type wit ++ str " was expected.")
+      ++ str " while type " ++ Genarg.pr_argument_type (unquote (rawwit wit)) ++ str " was expected.")
 
-  let cast wit v =
-    try val_cast wit v with CastError (wit, v) -> cast_error wit v
+  let prj : type a. a Val.tag -> Val.t -> a option = fun t v ->
+    let Val.Dyn (t', x) = v in
+    match Val.eq t t' with
+    | None -> None
+    | Some Refl -> Some x
+
+  let try_prj wit v = match prj (val_tag wit) v with
+  | None -> cast_error wit v
+  | Some x -> x
+
+  let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c =
+  fun wit v -> match wit with
+  | ExtraArg _ -> try_prj wit v
+  | ListArg t ->
+    let Val.Dyn (tag, v) = v in
+    begin match tag with
+    | Val.List tag ->
+      let map x = val_cast t (Val.Dyn (tag, x)) in
+      List.map map v
+    | _ -> cast_error wit (Val.Dyn (tag, v))
+    end
+  | OptArg t ->
+    let Val.Dyn (tag, v) = v in
+    begin match tag with
+    | Val.Opt tag ->
+      let map x = val_cast t (Val.Dyn (tag, x)) in
+      Option.map map v
+    | _ -> cast_error wit (Val.Dyn (tag, v))
+    end
+  | PairArg (t1, t2) ->
+    let Val.Dyn (tag, v) = v in
+    begin match tag with
+    | Val.Pair (tag1, tag2) ->
+      let (v1, v2) = v in
+      let v1 = Val.Dyn (tag1, v1) in
+      let v2 = Val.Dyn (tag2, v2) in
+      (val_cast t1 v1, val_cast t2 v2)
+    | _ -> cast_error wit (Val.Dyn (tag, v))
+    end
+
+  let cast (Topwit wit) v = val_cast wit v
 
 end