diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-03 16:50:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-03 16:50:40 +0200 |
| commit | b0e8bf149a9c620f2e2bd25f586fb41ee71aae0d (patch) | |
| tree | edcec459b613857728557f93c7b73ad7900ed0c3 /tactics/class_tactics.ml | |
| parent | a2a98a4015311af83edcf8fc87aa30a5318bead8 (diff) | |
[tactics] Fix summary registration of global hint variable.
It looks like `Class_tactics` forgot to register a couple of global
variables with the summary, thus creating problems on backtracking.
Fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5578
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 46d66b9d0..7ce6042c1 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -643,8 +643,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 @@ -973,8 +974,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 |