diff options
| author | Pierre-Marie Pédrot | 2016-01-17 01:08:21 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-17 01:13:23 +0100 |
| commit | 0d1345ea2423fc418a470786b0b33b80df3a67bc (patch) | |
| tree | 72aa847e645f0662c9f5241ea1f17ca4107390af /lib/genarg.ml | |
| parent | 43490147b0749f46eb90ff69c3bbdb3991fb526c (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.ml | 3 |
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 |
