aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/stdarg.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/stdarg.mli')
-rw-r--r--interp/stdarg.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 4159e6054..4792cda08 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -17,9 +17,11 @@ open Libnames
open Genredexpr
open Pattern
open Constrexpr
-open Misctypes
open Genarg
open Genintern
+open Locus
+
+type 'a and_short_name = 'a * lident option
val wit_unit : unit uniform_genarg_type