diff options
| author | Pierre-Marie Pédrot | 2017-03-23 08:38:00 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-03-23 11:54:48 +0100 |
| commit | f9526a2bcd05174b7adfe56b7375f0306a2a1e6d (patch) | |
| tree | 30b53903ae8d1d840090a204211b9ab7895ee879 /dev | |
| parent | 8cfe40dbc02156228a529c01190c50d825495013 (diff) | |
Fast path for implicit tactic solving.
We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions