aboutsummaryrefslogtreecommitdiff
path: root/interp/stdarg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/stdarg.ml')
-rw-r--r--interp/stdarg.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 492671fff0..d5f104b7f8 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -42,6 +42,8 @@ let wit_var =
let wit_ref = make0 "ref"
+let wit_smart_global = make0 ~dyn:(val_tag (topwit wit_ref)) "smart_global"
+
let wit_sort_family = make0 "sort_family"
let wit_constr =