diff options
author | 2013-04-11 21:21:33 +0000 | |
---|---|---|
committer | 2013-04-11 21:21:33 +0000 | |
commit | 0ea545ef3301be9590d9a1ab7d3eee35d7caec92 (patch) | |
tree | 2bd633d6c4226c33cb4e7ab69b39048696da385c /toplevel | |
parent | 1b9c67865370908efd1ef0250d6305920408697e (diff) |
Backport r16394 from 8.4:
- Fix caching of local hint database in typeclasses eauto which could
miss some hypotheses.
- Fix automatic solving of obligation in program, which was not trying
to solve obligations that had no undefined dependencies left.
Fix a warning in fourierR.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16395 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/obligations.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 092c329f3..7a0c498b2 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -833,14 +833,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 Int.Set.empty in let p = match oblset with | None -> (fun _ -> true) - | Some s -> (fun i -> Int.Set.mem i s) + | Some s -> set := s; + (fun i -> Int.Set.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 := Int.Set.union !set deps; + decr rem)) obls' in update_obls prg obls' !rem |