aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/context.mli')
-rw-r--r--kernel/context.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/context.mli b/kernel/context.mli
index ad6d645cd..048edef95 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -56,7 +56,7 @@ type rel_context = rel_declaration list
val empty_named_context : named_context
val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> Id.t list
+val vars_of_named_context : named_context -> Id.Set.t
val lookup_named : Id.t -> named_context -> named_declaration