diff options
| author | Pierre-Marie Pédrot | 2016-03-20 16:34:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 16:34:56 +0100 |
| commit | 1890a2cdc0dcda7335d7f81fc9ce77c0debc4324 (patch) | |
| tree | 92ef47814ba09193cac2cff57084dbb8fa9b739a /dev/include | |
| parent | 25bbce0e0cb841a7ad9d5c3e7ce33711b27bf41b (diff) | |
Fixing the classification of Tactic Notation.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions