coq/coq — pull request #27 by JasonGross (2014-06-23 00:51:28+00:00)
Title: More test-suite cases

3263 and 3395 are a bit slow.

I've run the test-suite, and get
```
success/decl_mode.v...Error! (should be accepted)
success/extraction.v...Error! (should be accepted)
success/intros.v...Error! (should be accepted)
success/namedunivs.v...Error! (should be accepted)
success/proof_using.v...Error! (should be accepted)
success/rewrite.v...Error! (should be accepted)
success/unification.v...Error! (should be accepted)
failure/subterm2.v...Error! (should be rejected)
failure/subterm3.v...Error! (should be rejected)
bugs/closed/1951.v...Error! (bug seems to be opened, please check)
bugs/closed/2080.v...Error! (bug seems to be opened, please check)
bugs/closed/2378.v...Error! (bug seems to be opened, please check)
bugs/closed/2406.v...Error! (bug seems to be opened, please check)
bugs/closed/2966.v...Error! (bug seems to be opened, please check)
bugs/closed/3036.v...Error! (bug seems to be opened, please check)
bugs/closed/HoTT_coq_034.v...Error! (bug seems to be opened, please check)
bugs/closed/HoTT_coq_036.v...Error! (bug seems to be opened, please check)
bugs/closed/HoTT_coq_044.v...Error! (bug seems to be opened, please check)
bugs/closed/HoTT_coq_054.v...Error! (bug seems to be opened, please check)
bugs/closed/HoTT_coq_064.v...Error! (bug seems to be opened, please check)
bugs/closed/HoTT_coq_098.v...Error! (bug seems to be opened, please check)
bugs/closed/HoTT_coq_110.v...Error! (bug seems to be opened, please check)
bugs/closed/HoTT_coq_113.v...Error! (bug seems to be opened, please check)
bugs/opened/1596.v...Error! (bug seems to be closed, please check)
bugs/opened/3300.v...Error! (bug seems to be closed, please check)
bugs/opened/3309.v...Error! (bug seems to be closed, please check)
bugs/opened/3329.v...Error! (bug seems to be closed, please check)
bugs/opened/3344.v...Error! (bug seems to be closed, please check)
bugs/opened/3392.v...Error! (bug seems to be closed, please check)
bugs/opened/HoTT_coq_078.v...Error! (bug seems to be closed, please check)
output/inference.v...Error! (unexpected output)
output/Notations.v...Error! (unexpected output)
output/simpl.v...Error! (unexpected output)
misc/universes...Error! (5/4 universes)
stm/Nijmegen_QArithSternBrocot_Zaux.v...Error! (should be accepted)
```

3392 fails because `Fail` doesn't catch anomalies correctly. The code
```coq
Fail Fail Defined.
Undo.
Defined.
```
will succeed, but won't catch a change that fixes the bug.