diff options
| author | Maxime Dénès | 2015-12-16 21:33:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-12-16 21:33:03 +0100 |
| commit | 793cf771e18be3d44d3fcf89998dec50fb8229f3 (patch) | |
| tree | d0d33aa6ae41d95d8c8c5b0e64c507a99eaf1ace /dev | |
| parent | b8d1e84e9326df34383e5e5c8c5842cb7013b935 (diff) | |
FIx parsing of tactic "simple refine".
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions