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

2 files changed, 17 insertions, 0 deletions

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