From b0e8bf149a9c620f2e2bd25f586fb41ee71aae0d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 3 Jun 2017 16:50:40 +0200
Subject: [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
---
 tactics/class_tactics.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 46d66b9d06..7ce6042c1a 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
-- 
cgit v1.2.3