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

3 files changed, 13 insertions, 7 deletions

diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index a8c79c31e4..02503ab475 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -504,7 +504,7 @@ let rec fourier gl=
                         (list_of_sign (pf_hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
-		        with NoIneq _ -> ())
+		        with NoIneq -> ())
               hyps;
     (* lineq = les inéquations découlant des hypothèses *)
     if !lineq=[] then Errors.error "No inequalities";
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 123b2a2efd..45a705f35a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -276,7 +276,7 @@ let make_hints g st only_classes sign =
     (PathEmpty, []) sign
   in Hint_db.add_list hintlist (Hint_db.empty st true)
 
-let autogoal_hints_cache : (Environ.named_context_val * hint_db) option ref = ref None
+let autogoal_hints_cache : (bool * Environ.named_context_val * hint_db) option ref = ref None
 let freeze () = !autogoal_hints_cache
 let unfreeze v = autogoal_hints_cache := v
 let init () = autogoal_hints_cache := None
@@ -293,9 +293,11 @@ let make_autogoal_hints =
   fun only_classes ?(st=full_transparent_state) g ->
     let sign = pf_filtered_hyps g in
       match freeze () with
-      | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints
+      | Some (onlyc, sign', hints) 
+	  when onlyc = only_classes && 
+	    Environ.eq_named_context_val sign sign' -> hints
       | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
-	  unfreeze (Some (sign, hints)); hints
+	  unfreeze (Some (only_classes, sign, hints)); hints
 	  
 let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
   { skft = fun sk fk {it = gl,hints; sigma=s} ->
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