diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index f5f1a459f4..ccdb980319 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -255,6 +255,10 @@ val make_all_name_different : env -> env val global_vars : env -> constr -> identifier list val global_vars_set_of_decl : env -> named_declaration -> Idset.t +(* Gives an ordered list of hypotheses, closed by dependencies, + containing a given set *) +val dependency_closure : env -> named_context -> Idset.t -> identifier list + (* Test if an identifier is the basename of a global reference *) val is_section_variable : identifier -> bool |