diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 13 | ||||
| -rw-r--r-- | pretyping/termops.mli | 4 |
2 files changed, 17 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 99252ce653..24ab23f4ae 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -1058,6 +1058,19 @@ let global_vars_set_of_decl env = function Idset.union (global_vars_set env t) (global_vars_set env c) +let dependency_closure env sign hyps = + if Idset.is_empty hyps then [] else + let (_,lh) = + Sign.fold_named_context_reverse + (fun (hs,hl) (x,_,_ as d) -> + if Idset.mem x hs then + (Idset.union (global_vars_set_of_decl env d) (Idset.remove x hs), + x::hl) + else (hs,hl)) + ~init:(hyps,[]) + sign in + List.rev lh + let default_x = id_of_string "x" let rec next_name_away_in_cases_pattern id avoid = 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 |