diff options
author | 2016-04-14 20:43:57 +0200 | |
---|---|---|
committer | 2016-05-04 13:47:12 +0200 | |
commit | a2a8840a4fe1b3d6c6dbc27b5521b28bd319ff42 (patch) | |
tree | 88108ed4457cb0b573e468752619a2939085dd1a /interp | |
parent | de4b9b68445d9f3e48da789404cbdfcd89214585 (diff) |
More toplevel value representation sharing.
Diffstat (limited to 'interp')
-rw-r--r-- | interp/stdarg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 9e85dbaf3..2a7d52e3a 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -27,7 +27,7 @@ let wit_string : string uniform_genarg_type = make0 "string" let wit_pre_ident : string uniform_genarg_type = - make0 "preident" + make0 ~dyn:(val_tag (topwit wit_string)) "preident" (** Aliases for compatibility *) |