diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-04-09 07:36:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-04-09 07:37:19 +0200 |
| commit | 400d3dcca26bba32d6e170ef36468e6c5425a2ed (patch) | |
| tree | 41aa9e763bc2bd08599490e9783518318c0796b2 | |
| parent | 19ca8f80e7e35e8f6c41c99bd311b3c7df2033e2 (diff) | |
Fix caching of local hintdb in typeclasses eauto.
| -rw-r--r-- | tactics/class_tactics.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e97a42e6e..98266a4b6 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -350,7 +350,9 @@ let make_autogoal_hints = let sign = pf_filtered_hyps g in let (onlyc, sign', cached_hints) = !cache in if onlyc == only_classes && - (sign == sign' || Environ.eq_named_context_val sign sign') then + (sign == sign' || Environ.eq_named_context_val sign sign') + && Hint_db.transparent_state cached_hints == st + then cached_hints else let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in |