aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-17 02:56:14 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-17 03:01:58 +0100
commit820a282fde5cb4233116ce2cda927fda2f36097d (patch)
tree9893efb3b59d836a61b09853a0c94ba798e9c0b2 /lib/genarg.mli
parentd3ee6b2fbcd0fbb666af7f1920446e809e8d6e1e (diff)
Moving val_cast to Tacinterp.
Diffstat (limited to 'lib/genarg.mli')
-rw-r--r--lib/genarg.mli5
1 files changed, 0 insertions, 5 deletions
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