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
---
 tactics/class_tactics.ml4 | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'tactics')

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} ->
-- 
cgit v1.2.3