From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 1 Jun 2018 02:37:15 +0200
Subject: [api] Remove Misctypes.

We move the last 3 types to more adequate places.
---
 interp/stdarg.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'interp/stdarg.ml')

diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 7a7bb9a848..7b01b6dc1c 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -11,6 +11,8 @@
 open Genarg
 open Geninterp
 
+type 'a and_short_name = 'a * Names.lident option
+
 let make0 ?dyn name =
   let wit = Genarg.make0 name in
   let () = register_val0 wit dyn in
-- 
cgit v1.2.3