diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 30 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 |
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. } |