From 58630ad9a0b94a804a39a3d99f982965292692c7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 21 May 2018 23:54:55 +0200
Subject: [api] Misctypes removal: miscellaneous aliases.

---
 kernel/names.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/names.mli')

diff --git a/kernel/names.mli b/kernel/names.mli
index f988b559a8..4eb5adb62f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -605,3 +605,9 @@ type evaluable_global_reference =
   | EvalConstRef of Constant.t
 
 val eq_egr : evaluable_global_reference ->  evaluable_global_reference -> bool
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
-- 
cgit v1.2.3