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.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index 621a9931d..c3fd8962e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -101,6 +101,8 @@ let fold_rel_context f env ~init = let named_context_of_val c = c.env_named_ctx +let ids_of_named_context_val c = Id.Map.domain c.env_named_map + (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) -- cgit v1.2.3