Environ: export API to transitively close a set of section variables

2 files changed, 20 insertions, 14 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 679c807d65..105eb7da1b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -261,21 +261,23 @@ let global_vars_set env constr =
    contains the variables of the set [ids], and recursively the variables
    contained in the types of the needed variables. *)
 
+let really_needed env needed =
+  Context.fold_named_context_reverse
+    (fun need (id,copt,t) ->
+      if Id.Set.mem id need then
+        let globc =
+          match copt with
+            | None -> Id.Set.empty
+            | Some c -> global_vars_set env c in
+        Id.Set.union
+          (global_vars_set env t)
+          (Id.Set.union globc need)
+      else need)
+    ~init:needed
+    (named_context env)
+
 let keep_hyps env needed =
-  let really_needed =
-    Context.fold_named_context_reverse
-      (fun need (id,copt,t) ->
-        if Id.Set.mem id need then
-          let globc =
-	    match copt with
-	      | None -> Id.Set.empty
-	      | Some c -> global_vars_set env c in
-	  Id.Set.union
-            (global_vars_set env t)
-	    (Id.Set.union globc need)
-        else need)
-      ~init:needed
-      (named_context env) in
+  let really_needed = really_needed env needed in
   Context.fold_named_context
     (fun (id,_,_ as d) nsign ->
       if Id.Set.mem id really_needed then add_named_decl d nsign
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 66cb03a1cd..652cd59bf1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -171,6 +171,10 @@ val global_vars_set : env -> constr -> Id.Set.t
 (** the constr must be a global reference *)
 val vars_of_global : env -> constr -> Id.Set.t
 
+(** closure of the input id set w.r.t. dependency *)
+val really_needed : env -> Id.Set.t -> Id.Set.t
+
+(** like [really_needed] but computes a well ordered named context *)
 val keep_hyps : env -> Id.Set.t -> section_context
 
 (** {5 Unsafe judgments. }