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/eauto.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/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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 |