aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/names.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.mli')
-rw-r--r--kernel/names.mli6
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli
index f988b559a..4eb5adb62 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