diff options
| author | Pierre-Marie Pédrot | 2014-03-28 14:12:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-28 14:53:54 +0100 |
| commit | 91eb9e8cd5c68d5a71c07787900a8bb6d0481ba9 (patch) | |
| tree | 848fd192b140f1d99937fcb7c0b8898ffb8d9e57 /dev/header | |
| parent | 8934da82d30fee8205fe1694ed601817ff858e5c (diff) | |
Lighter interface for creating refining tactics.
Diffstat (limited to 'dev/header')
0 files changed, 0 insertions, 0 deletions