aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-11 21:40:23 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-14 18:23:32 +0100
commit67b9b34d409c793dc449104525684852353ee064 (patch)
tree50a061e5cbaea7507c226d94d33fdfc5d10bc5ee /lib/genarg.mli
parent00e27eac9fe207d754952c1ddb0e12861ee293c9 (diff)
Removing ident and var generic arguments.
Diffstat (limited to 'lib/genarg.mli')
-rw-r--r--lib/genarg.mli4
1 files changed, 1 insertions, 3 deletions
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 674ee97ae..8d929f9f6 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -212,10 +212,8 @@ val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a
type argument_type =
(** Basic types *)
- | IdentArgType
- | VarArgType
- (** Specific types *)
| ConstrArgType
+ (** Specific types *)
| ListArgType of argument_type
| OptArgType of argument_type
| PairArgType of argument_type * argument_type