diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-11 21:21:33 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-11 21:21:33 +0000 |
| commit | 0ea545ef3301be9590d9a1ab7d3eee35d7caec92 (patch) | |
| tree | 2bd633d6c4226c33cb4e7ab69b39048696da385c /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 123b2a2ef..45a705f35 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} -> |