From 0ea545ef3301be9590d9a1ab7d3eee35d7caec92 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 11 Apr 2013 21:21:33 +0000
Subject: 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
---
 toplevel/obligations.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 092c329f39..7a0c498b27 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
-- 
cgit v1.2.3