diff options
Diffstat (limited to 'typing')
| -rw-r--r-- | typing/outcometree.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/typing/outcometree.mli b/typing/outcometree.mli index 80966f4053..6d65d577d1 100644 --- a/typing/outcometree.mli +++ b/typing/outcometree.mli @@ -59,11 +59,8 @@ type out_value = | Oval_stuff of string | Oval_tuple of out_value list | Oval_variant of string * out_value option -(* GENERIC (dynamic values are not longer printable...) - | Oval_dynamic of out_value option * out_type -/GENERIC *) (* DYN *) - | Oval_dynamic of out_type + | Oval_dynamic of out_value option * out_type (* /DYN *) type out_class_type = |