diff options
| author | Pierre-Marie Pédrot | 2014-09-05 14:40:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-05 15:32:03 +0200 |
| commit | 581cbe36191901f1dc234fe77d619abfe7b8de34 (patch) | |
| tree | 9d160ef01f541970d2a9fd6788a3377622794600 /kernel | |
| parent | 466c25ea43149deedf50e0105a6d1e69db91c8fd (diff) | |
Adding a Ftactic module for potentially focussing tactics.
The code for the module was moved from Tacinterp. We still expose partially
the implementation of the Ftactic.t type, for the sake of simplicity. It may
be dangerous if used improperly though.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions