coq/coq — pull request #12 by JasonGross (2014-04-05 22:06:28+00:00)
Title: Add test-suite cases for bugs fixed in the past few days

The only way I could figure to test for "not stack overflow" was `Timeout 2` (or there-abouts); I'm not sure if this is permitted in the test-suite. I've made a separate commit for each test-suite case, so you can merge some of them without others.

The current state of the test suite is:
```
make[3]: Entering directory `/afs/csail.mit.edu/u/j/jgross/coq/test-suite'
make[3]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq/test-suite'
make[2]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq/test-suite'
if grep -F 'Error!' test-suite/summary.log ; then false; fi
success/decl_mode.v...Error! (should be accepted)
success/proof_using.v...Error! (should be accepted)
failure/subterm2.v...Error! (should be rejected)
failure/subterm3.v...Error! (should be rejected)
bugs/closed/1041.v...Error! (bug seems to be opened, please check)
bugs/closed/2406.v...Error! (bug seems to be opened, please check)
bugs/closed/3036.v...Error! (bug seems to be opened, please check)
bugs/closed/3251.v...Error! (bug seems to be opened, please check)
output/Errors.v...Error! (unexpected output)
output/Notations.v...Error! (unexpected output)
output/simpl.v...Error! (unexpected output)
stm/Nijmegen_QArithSternBrocot_Zaux.v...Error! (should be accepted)
make[1]: *** [test-suite] Error 1
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/coq'
make: *** [submake] Error 2
```
and for `validate`:
```
Checking library: Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic
checking cst: Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic.lor
checking cst: Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic.land
checking cst: Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic.lxor
checking cst: Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic.mk_zn2z_ops
checking cst: Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic.mk_zn2z_ops_karatsuba
checking cst: Coq.Numbers.Cyclic.DoubleCyclic.DoubleCyclic.spec_ww_add_mul_div
Type error: CantApplyBadType
make[1]: *** [validate] Error 1
```