diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-04-11 14:24:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
| commit | 46388674943195e5d64340d54553c98d5698a68e (patch) | |
| tree | 6bea61e9695be2369fbf026a28524ed2377278d5 | |
| parent | 30d0a2333c1b701bddef35652009fb258f08153c (diff) | |
Fix incorrect caching of local hints w.r.t sections
| -rw-r--r-- | tactics/class_tactics.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index fbaebdf15..2cee9de15 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -497,15 +497,17 @@ type newautoinfo = search_cut : hints_path; search_hints : hint_db; } -let autogoal_cache = ref (true, Context.Named.empty, +let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty, Hint_db.empty full_transparent_state true) let make_autogoal_hints' only_classes ?(st=full_transparent_state) g = let open Proofview in let open Tacmach.New in let sign = Goal.hyps g in - let (onlyc, sign', cached_hints) = !autogoal_cache in - if onlyc == only_classes && + let (dir, onlyc, sign', cached_hints) = !autogoal_cache in + let cwd = Lib.cwd () in + if DirPath.equal cwd dir && + (onlyc == only_classes) && Context.Named.equal sign sign' && Hint_db.transparent_state cached_hints == st then cached_hints @@ -513,7 +515,7 @@ let make_autogoal_hints' only_classes ?(st=full_transparent_state) g = let hints = make_hints {it = Goal.goal g; sigma = project g} st only_classes sign in - autogoal_cache := (only_classes, sign, hints); hints + autogoal_cache := (cwd, only_classes, sign, hints); hints let make_autogoal' ?(st=full_transparent_state) only_classes cut i g = let hints = make_autogoal_hints' only_classes ~st g in |