diff options
author | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /plugins/subtac | |
parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'plugins/subtac')
-rw-r--r-- | plugins/subtac/subtac_obligations.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index d8f46098..7a4916fa 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -559,14 +559,18 @@ and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in let rem = ref rem in let obls' = Array.copy obls in + let set = ref Intset.empty in let p = match oblset with | None -> (fun _ -> true) - | Some s -> (fun i -> Intset.mem i s) + | Some s -> set := s; + (fun i -> Intset.mem i !set) in let _ = Array.iteri (fun i x -> - if p i && solve_obligation_by_tac prg obls' i tac then - decr rem) + if p i && solve_obligation_by_tac prg obls' i tac then + let deps = dependencies obls i in + (set := Intset.union !set deps; + decr rem)) obls' in update_obls prg obls' !rem |