From 87580ced814f668f8c61814a692e05b39bc5c5f7 Mon Sep 17 00:00:00 2001 From: barras Date: Thu, 27 Nov 2008 13:29:10 +0000 Subject: fixing problem with CompCert: reordering resulting from tac change was not closed w.r.t. dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11634 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/termops.ml | 13 +++++++++++++ pretyping/termops.mli | 4 ++++ 2 files changed, 17 insertions(+) (limited to 'pretyping') diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 99252ce65..24ab23f4a 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 f5f1a459f..ccdb98031 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 -- cgit v1.2.3