aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/decl_kinds.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/decl_kinds.mli')
-rw-r--r--intf/decl_kinds.mli5
1 files changed, 4 insertions, 1 deletions
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 29972f2f4..c117baf3f 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -10,7 +10,10 @@
type locality = Discharge | Local | Global
-type binding_kind = Explicit | Implicit
+type implicit_status = Explicit | Implicit
+
+type binding_kind = implicit_status
+(** @deprecated Alias type *)
type polymorphic = bool