diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-11 16:33:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-11 16:33:26 +0200 |
| commit | 2bcae5b7a22019718973f65cafd271f735d3d85b (patch) | |
| tree | e74acd37e10d7045de93e9f7a0569852a69cb7ad | |
| parent | d226adf01f20ea946bbeac4d4c5cde75a4d77f32 (diff) | |
Fix test-suite file 5123 to fail in case of regression
| -rw-r--r-- | test-suite/bugs/closed/5123.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v index c171a10d1..bcde510ee 100644 --- a/test-suite/bugs/closed/5123.v +++ b/test-suite/bugs/closed/5123.v @@ -21,6 +21,7 @@ Goal True. unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. all:cycle 2. eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) + Focus 5. Abort. Goal True. @@ -28,4 +29,5 @@ Goal True. Unshelve. all:cycle 3. eapply existT. (*This does no typeclass resultion, which is correct.*) + Focus 5. Abort.
\ No newline at end of file |