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 /kernel/nativelambda.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 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions