Fix name of some Int31 operations in native compiler.
Fix exponential behavior in native compiler with retroknowledge.
Adapt test-suite to -I is ML only
Adapt coq_makefile build rules to new -R -I semantic
Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fix for Rocq/Rational.)"

This reverts commit 7d3ce4012a53b123dac95381bf46aac65f865d69.

Conflicts:
	CHANGES
Add another critical bug to the test-suite.

I have a fix, I'm reviewing it because there may be other bugs around.
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