From b772c323f62b322c9b0a4ab90c7de8b1e2066bae Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 10 Sep 2017 02:21:03 +0200 Subject: Efficient computation of the names contained in an environment. --- kernel/environ.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel/environ.mli') diff --git a/kernel/environ.mli b/kernel/environ.mli index 377c61de2..2667ad7ca 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -80,6 +80,7 @@ val fold_rel_context : val named_context_of_val : named_context_val -> Context.Named.t val val_of_named_context : Context.Named.t -> named_context_val val empty_named_context_val : named_context_val +val ids_of_named_context_val : named_context_val -> Id.Set.t (** [map_named_val f ctxt] apply [f] to the body and the type of -- cgit v1.2.3