aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/genarg.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-30 12:09:21 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-30 12:20:23 +0200
commitc0aefc5323cb4393297adcaffd2967ab93ab815e (patch)
tree6e9d4dad66807a231083e9965d2e22436b56a793 /lib/genarg.mli
parent051c9a8a1112174769670cb0dc8cebb85ccb803c (diff)
Ensuring that the type of base generic arguments contain triples.
Diffstat (limited to 'lib/genarg.mli')
-rw-r--r--lib/genarg.mli10
1 files changed, 5 insertions, 5 deletions
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 30b96c700..6cc7893dc 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -70,15 +70,15 @@ ExtraArgType of string '_a '_b
module ArgT :
sig
- type 'a tag
- val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
- val repr : 'a tag -> string
- type any = Any : 'a tag -> any
+ type ('a, 'b, 'c) tag
+ val eq : ('a1, 'b1, 'c1) tag -> ('a2, 'b2, 'c2) tag -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
+ val repr : ('a, 'b, 'c) tag -> string
+ type any = Any : ('a, 'b, 'c) tag -> any
val name : string -> any option
end
type (_, _, _) genarg_type =
-| ExtraArg : ('a * 'b * 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
+| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->