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/auto.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/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 4 |
1 files changed, 4 insertions, 0 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 |