diff options
| -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 e97a42e6e4..98266a4b6c 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 |