Add a test-case for bug #3314 proving False
Move closed bug 3314
Add many more cases to the test-suite

I'd add more, but I'm tired and it's late and I should sleep.  Maybe
I'll pick up at 3279 (working down) another day.

Bug 3344 is broken; [Fail Defined.] says that [Defined] has not failed,
even though it raises an anomaly.  So there's no way I can think of to
test it.  I've left it in the [opened] directory anyway.
fix handling of side effects in abstract (fixes QArithSternBrocot)

The right fix should probably be to remove the build_constant_by_tactic
function and only use the build_by_tactic one
In generalized rewrite, avoid retyping completely and constantly the conclusion, and results of
unifying the lemma with subterms. Using Retyping.get_type_of instead results in 3x
speedup in Ncring_polynom.
- Fix bug #3368, due to wrong use of the Cst_stack for projections.
- Monomorphize Cst_stack to 'a = constr.
- Add corresponding debug printer.
Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into trunk