diff options
| author | Pierre-Marie Pédrot | 2014-10-01 18:02:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-10-01 18:02:10 +0200 |
| commit | 03b631ea3eeeaab9054c34d9121c0a75fabea72c (patch) | |
| tree | feb7e4303af49c165f0f8a66780cff576b7d35d4 /lib | |
| parent | 14120a1d0b509bfc02e275d9f1fd07d61d9fa9f3 (diff) | |
Removing test for bug #2080.
Naming a Ltac definition like a built-in tactic used to fail, but now only
spits out a warning. This is too complicated to test...
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions