aboutsummaryrefslogtreecommitdiffhomepage
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 274ea6213..45dec5112 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -50,6 +50,8 @@ let wit_ref = make0 "ref"
let wit_quant_hyp = make0 "quant_hyp"
+let wit_sort_family = make0 "sort_family"
+
let wit_constr =
make0 "constr"