aboutsummaryrefslogtreecommitdiff
path: root/lib/genarg.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-01-17 01:08:21 +0100
committerPierre-Marie Pédrot2016-01-17 01:13:23 +0100
commit0d1345ea2423fc418a470786b0b33b80df3a67bc (patch)
tree72aa847e645f0662c9f5241ea1f17ca4107390af /lib/genarg.ml
parent43490147b0749f46eb90ff69c3bbdb3991fb526c (diff)
Temporary commit getting rid of Obj.magic unsafety for Genarg.
This will allow an easier landing of the rewriting of Genarg.
Diffstat (limited to 'lib/genarg.ml')
-rw-r--r--lib/genarg.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/genarg.ml b/lib/genarg.ml
index c2c1014f17..5efb074440 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -117,6 +117,9 @@ type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
+let arg_list wit = ListArgType wit
+let arg_opt wit = OptArgType wit
+
type ('a, 'b, 'c, 'l) cast = Obj.t
let raw = Obj.obj