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 | |
| 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...
| -rw-r--r-- | test-suite/bugs/closed/2080.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/2080.v b/test-suite/bugs/closed/2080.v deleted file mode 100644 index 62c42c8c31..0000000000 --- a/test-suite/bugs/closed/2080.v +++ /dev/null @@ -1 +0,0 @@ -Fail Ltac clear h := inversion h; clear h. |