diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-14 00:26:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-14 10:28:27 +0200 |
| commit | 684dd06c538ea6024e5dd01bfc6eb416b08ddc14 (patch) | |
| tree | 4f5b011b96b0afea2a5d2b1877df8be64f7e898d /tactics | |
| parent | 3b6d89acf4f233d0ed33f89c4e60bcd68e0e2820 (diff) | |
Removing a variable warned unused.
Diffstat (limited to 'tactics')
0 files changed, 0 insertions, 0 deletions