diff options
| author | Théo Zimmermann | 2019-09-17 14:12:05 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-09-18 15:43:16 +0200 |
| commit | 2cff572ecea5846b23370c6912ff488bb099e761 (patch) | |
| tree | 59d57bc46ef152c1c815f5cae470abeaaeda8192 /dev/doc | |
| parent | c18f04422cb0827994e8d7aecc384a2c448a61c9 (diff) | |
Fix syntax of reduction tactics when listing qualid to reduce or not.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions