Fix parsing of :>> and backtrack correctly on the cache of hints for local contexts

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14688 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 21 insertions, 8 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5fe558adf..c9700cdf0 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -378,10 +378,11 @@ GEXTEND Gram
   ;
   of_type_with_opt_coercion:
     [ [ ":>>" -> Some false
-    | ":>" -> Some true
-    | ":"; ">" -> Some true
-    | ":"; ">"; ">" -> Some false
-    | ":" -> None ] ]
+	| ":>"; ">" -> Some false
+	| ":>" -> Some true
+	| ":"; ">"; ">" -> Some false
+	| ":"; ">" -> Some true
+	| ":" -> None ] ]
   ;
 END
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 1f8ee3af6..c33299397 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -273,15 +273,27 @@ let make_hints g st only_classes sign =
 	 (PathOr (paths, path), hint @ hints))
     (PathEmpty, []) sign
   in Hint_db.add_list hintlist (Hint_db.empty st true)
+
+let autogoal_hints_cache : (Environ.named_context_val * hint_db) option ref = ref None
+let freeze () = !autogoal_hints_cache
+let unfreeze v = autogoal_hints_cache := v
+let init () = autogoal_hints_cache := None
+
+let _ = init ()
+
+let _ =
+  Summary.declare_summary "autogoal-hints-cache"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init }
     
 let make_autogoal_hints = 
-  let res = ref None in
-    fun only_classes ?(st=full_transparent_state) g ->
+  fun only_classes ?(st=full_transparent_state) g ->
     let sign = pf_filtered_hyps g in
-      match !res with
+      match freeze () with
       | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints
       | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
-	  res := Some (sign, hints); hints
+	  unfreeze (Some (sign, hints)); hints
 	  
 let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
   { skft = fun sk fk {it = gl,hints; sigma=s} ->