aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-14 20:43:57 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-04 13:47:12 +0200
commita2a8840a4fe1b3d6c6dbc27b5521b28bd319ff42 (patch)
tree88108ed4457cb0b573e468752619a2939085dd1a /interp
parentde4b9b68445d9f3e48da789404cbdfcd89214585 (diff)
More toplevel value representation sharing.
Diffstat (limited to 'interp')
-rw-r--r--interp/stdarg.ml2
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 *)