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.

5 files changed, 88 insertions, 14 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d7de6c4fb5..65b2615b6b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -416,6 +416,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
     "nocore" amongst the databases. *)
 
 let trivial ?(debug=Off) lems dbnames =
+  Hints.wrap_hint_warning @@
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
@@ -427,6 +428,7 @@ let trivial ?(debug=Off) lems dbnames =
   end
 
 let full_trivial ?(debug=Off) lems =
+  Hints.wrap_hint_warning @@
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
@@ -501,6 +503,7 @@ let search d n mod_delta db_list local_db =
 let default_search_depth = ref 5
 
 let delta_auto debug mod_delta n lems dbnames =
+  Hints.wrap_hint_warning @@
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
@@ -524,6 +527,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n
 let default_auto = auto !default_search_depth [] []
 
 let delta_full_auto ?(debug=Off) mod_delta n lems =
+  Hints.wrap_hint_warning @@
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 3456d13bbe..2b183a9d37 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -934,6 +934,9 @@ module Search = struct
                                             | Some i -> str ", with depth limit " ++ int i));
     tac
 
+  let eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints =
+    Hints.wrap_hint_warning @@ eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints
+
   let run_on_evars env evm p tac =
     match evars_to_goals p evm with
     | None -> None (* This happens only because there's no evar having p *)
@@ -1143,15 +1146,19 @@ let resolve_typeclass_evars debug depth unique env evd filter split fail =
                       (initial_select_evars filter) evd split fail
 
 let solve_inst env evd filter unique split fail =
-  resolve_typeclass_evars
+  let ((), sigma) = Hints.wrap_hint_warning_fun env evd begin fun evd ->
+    (), resolve_typeclass_evars
     (get_typeclasses_debug ())
     (get_typeclasses_depth ())
     unique env evd filter split fail
+  end in
+  sigma
 
 let _ =
   Hook.set Typeclasses.solve_all_instances_hook solve_inst
 
 let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
+  let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma ->
   let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
   let (gl,t,sigma) =
     Goal.V82.mk_goal sigma nc gl Store.empty in
@@ -1169,7 +1176,9 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
   let evd = sig_sig gls' in
   let t' = mkEvar (ev, Array.of_list subst) in
   let term = Evarutil.nf_evar evd t' in
-    evd, term
+  term, evd
+  end in
+  (sigma, term)
 
 let _ =
   Hook.set Typeclasses.solve_one_instance_hook
@@ -1205,6 +1214,7 @@ let is_ground c =
 
 let autoapply c i =
   let open Proofview.Notations in
+  Hints.wrap_hint_warning @@
   Proofview.Goal.enter begin fun gl ->
   let hintdb = try Hints.searchtable_map i with Not_found ->
     CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ "."))
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 80d07c5c03..5067315d08 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -409,7 +409,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
 (* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *)
 
 let eauto_with_bases ?(debug=Off) np lems db_list =
-  tclTRY (e_search_auto debug np lems db_list)
+  Proofview.V82.of_tactic (Hints.wrap_hint_warning (Proofview.V82.tactic (tclTRY (e_search_auto debug np lems db_list))))
 
 let eauto ?(debug=Off) np lems dbnames =
   let db_list = make_db_list dbnames in
@@ -420,8 +420,8 @@ let full_eauto ?(debug=Off) n lems gl =
   tclTRY (e_search_auto debug n lems db_list) gl
 
 let gen_eauto ?(debug=Off) np lems = function
-  | None -> Proofview.V82.tactic (full_eauto ~debug np lems)
-  | Some l -> Proofview.V82.tactic (eauto ~debug np lems l)
+  | None -> Hints.wrap_hint_warning (Proofview.V82.tactic (full_eauto ~debug np lems))
+  | Some l -> Hints.wrap_hint_warning (Proofview.V82.tactic (eauto ~debug np lems l))
 
 let make_depth = function
   | None -> !default_search_depth
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.")))
diff --git a/tactics/hints.mli b/tactics/hints.mli
index c49ca2094a..d63efea27d 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -282,6 +282,15 @@ val make_db_list : hint_db_name list -> hint_db list
 val typeclasses_db : hint_db_name
 val rewrite_db : hint_db_name
 
+val wrap_hint_warning : 'a Proofview.tactic -> 'a Proofview.tactic
+(** Use around toplevel calls to hint-using tactics, to enable the tracking of
+    non-imported hints. Any tactic calling [run_hint] must be wrapped this
+    way. *)
+
+val wrap_hint_warning_fun : env -> evar_map ->
+  (evar_map -> 'a * evar_map) -> 'a * evar_map
+(** Variant of the above for non-tactics *)
+
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t