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.
CoqIDE: removing a timer may raise an exception
CoqIDE: options for syntax highlighting
Dumpglob: factor out reference dumping.

Factored out all functions that dump references to use one function
"dump_ref"
Have the feedback bus as a backend for dumping globs.
better description of bug 3251
Fix guard condition for nested cofixpoints.

There were actually two problems, one of them being clearly unsound.
To make sure that this does not show up somewhere else in the code, it would
be better to resort to an abstraction keeping in sync the environment and the
De Bruijn index of the current cofixpoints, like guard_env does for fixpoints.
Fix guard condition for nested cofixpoints in checker.
Closing bug #3260
adding a new grammar entry for clauses
Fixing missing headers.