Make the warning for non-imported hints compatible with internal backtracking.

This prevents outputing false positives when the hints are discarded during
proof search. Note that this is not sychronized with Ltac backtrack though,
so your tactic may end up not using the hint and warning about it because
a run of some auto function succeeded.

1 files changed, 60 insertions, 9 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 3835dee299..c0ba363360 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1579,25 +1579,76 @@ let print_mp mp =
 
 let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
 
+let hint_trace = Evd.Store.field ()
+
+let log_hint h =
+  let open Proofview.Notations in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let store = get_extra_data sigma in
+  match Store.get store hint_trace with
+  | None ->
+    (** All calls to hint logging should be well-scoped *)
+    assert false
+  | Some trace ->
+    let trace = KNmap.add h.uid h trace in
+    let store = Store.set store hint_trace trace in
+    Proofview.Unsafe.tclEVARS (set_extra_data store sigma)
+
 let warn_non_imported_hint =
   CWarnings.create ~name:"non-imported-hint" ~category:"automation"
          (fun (hint,mp) ->
           strbrk "Hint used but not imported: " ++ hint ++ print_mp mp)
 
-let warn h x =
-  let open Proofview in
-  tclBIND tclENV     (fun env   ->
-  tclBIND tclEVARMAP (fun sigma ->
-          let hint = pr_hint env sigma h in
-          let (mp, _, _) = KerName.repr h.uid in
-          warn_non_imported_hint (hint,mp);
-          Proofview.tclUNIT x))
+let warn env sigma h =
+  let hint = pr_hint env sigma h in
+  let (mp, _, _) = KerName.repr h.uid in
+  warn_non_imported_hint (hint,mp)
+
+let wrap_hint_warning t =
+  let open Proofview.Notations in
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let store = get_extra_data sigma in
+  let old = Store.get store hint_trace in
+  let store = Store.set store hint_trace KNmap.empty in
+  Proofview.Unsafe.tclEVARS (set_extra_data store sigma) >>= fun () ->
+  t >>= fun ans ->
+  Proofview.tclENV >>= fun env ->
+  Proofview.tclEVARMAP >>= fun sigma ->
+  let store = get_extra_data sigma in
+  let hints = match Store.get store hint_trace with
+  | None -> assert false
+  | Some hints -> hints
+  in
+  let () = KNmap.iter (fun _ h -> warn env sigma h) hints in
+  let store = match old with
+  | None -> Store.remove store hint_trace
+  | Some v -> Store.set store hint_trace v
+  in
+  Proofview.Unsafe.tclEVARS (set_extra_data store sigma) >>= fun () ->
+  Proofview.tclUNIT ans
+
+let wrap_hint_warning_fun env sigma t =
+  let store = get_extra_data sigma in
+  let old = Store.get store hint_trace in
+  let store = Store.set store hint_trace KNmap.empty in
+  let (ans, sigma) = t (set_extra_data store sigma) in
+  let store = get_extra_data sigma in
+  let hints = match Store.get store hint_trace with
+  | None -> assert false
+  | Some hints -> hints
+  in
+  let () = KNmap.iter (fun _ h -> warn env sigma h) hints in
+  let store = match old with
+  | None -> Store.remove store hint_trace
+  | Some v -> Store.set store hint_trace v
+  in
+  (ans, set_extra_data store sigma)
 
 let run_hint tac k = match !warn_hint with
 | `LAX -> k tac.obj
 | `WARN ->
   if is_imported tac then k tac.obj
-  else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x)
+  else Proofview.tclTHEN (log_hint tac) (k tac.obj)
 | `STRICT ->
   if is_imported tac then k tac.obj
   else Proofview.tclZERO (UserError (None, (str "Tactic failure.")))