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/hints.mli | |
| 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/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 9 |
1 files changed, 9 insertions, 0 deletions
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 |