diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-19 17:39:33 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-19 17:39:33 +0200 |
| commit | bed646cc2ff5429661959492959ccd6835b581d4 (patch) | |
| tree | 9de3797350d4e373c6e4c26b1930d3d071dfbade /tactics/class_tactics.ml | |
| parent | 9c6b492355d82b6346176d884f593bbbf5bde67f (diff) | |
| parent | b0e8bf149a9c620f2e2bd25f586fb41ee71aae0d (diff) | |
Merge PR#727: [tactics] Fix summary registration of global hint variable.
Diffstat (limited to 'tactics/class_tactics.ml')
| -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 2faf1e0ec..5fbf59b81 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -649,8 +649,9 @@ module V85 = struct Goal.V82.hyps gls.Evd.sigma (sig_it gls) let make_autogoal_hints = - let cache = ref (true, Environ.empty_named_context_val, - Hint_db.empty full_transparent_state true) + let cache = Summary.ref ~name:"make_autogoal_hints_cache" + (true, Environ.empty_named_context_val, + Hint_db.empty full_transparent_state true) in fun only_classes ?(st=full_transparent_state) g -> let sign = pf_filtered_hyps g in @@ -979,8 +980,9 @@ module Search = struct search_hints : hint_db; } (** Local hints *) - let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty, - Hint_db.empty full_transparent_state true) + let autogoal_cache = Summary.ref ~name:"autogoal_cache" + (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 |