Add a regression test for bug 3001
Test case for bug #3217

It was fixed in c3feef4ed5dec126f1144dec91eee9c0f0522a94.

The test case uses [Timeout 2] to test for "Coq runs instantaneously
rather than running out of memory".  Hopefully this is robust enough.
Test case for bug 3262

Closed in f65fa9de8a4c9c12d933188a755b51508bd51921

I used [Timeout 2 Fail] to test the difference between immediate failure
and stack overflow.  Hopefully this is robust enough.
Test case for 3164

Closed in 69c4d0fd7b8325187e8da697a9c283594047d.

I used [Timeout 2] to distinguish between stack overflow and immediate
return.
Test case for bug 3037

Closed in 4a8950ec7a0d9f2b216e67e69b446c064590a8e9
Define [projT3] and [proj3_sig]

Also allow [projT1]/[projT2] to work for [sigT2]s and
[proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions.

This closes Bug 3044.
This closes Pull Request #4.
No more Coersion in Init.
By resolution of the CoqWG, instantiate must not be used now that refine works
coqtop -batch refuses Back 1 but accepts Undo.