diff options
| author | Pierre-Marie Pédrot | 2018-07-27 16:21:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-26 14:40:17 +0200 |
| commit | f2840256990809ef83051dbed53d337688ef2a7b (patch) | |
| tree | b434263332fe587df9e623c7468ab858842da170 /tactics/class_tactics.ml | |
| parent | 871c694e5395e85296f4c61ba4039f04704b20b3 (diff) | |
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.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 14 |
1 files changed, 12 insertions, 2 deletions
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 ^ ".")) |