Taming the simpl evar hack that used to use negative evars.
Now we just generate evars in the given evar map.

At least, the test-suite isn't broken...

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16782 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing almost all new_untyped_evar, and a bunch of Evd.add.
Ultimately all evars should be created with respect to a given
evar map, instead of using a global counter.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16783 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing unused code from Term_dnet.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16784 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing the last global evar generation in Term_dnet. The very
fact that the previous implementation was working is still black
magic to me, as evars may have collided in intriguing ways...

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16785 85f007b7-540e-0410-9357-904b9bb8a0f7
At least made the evar type opaque! There are still 5 remaining unsafe
casts of ints to evars.

- 2 in Evarutil and Goal which are really needed, even though the Goal
one could (and should) be removed;
- 2 in G_xml and Detyping that are there for completeness sake, but
that might be made anomalies altogether;
- 1 in Newring which is quite dubious at best, and should be fixed.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
Get rid of the uses of deprecated OCaml elements (still remaining compatible with OCaml 3.12.1).

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
Made the filename of compiled files explicit, i.e. add a ./ prefix
whenever the filename was given alone. This caused strange behaviour
of coqtop that was compiling stuff we didn't want to just because
it was somewhere in its loadpath.

This is why FingerTree was not compiling, btw, as it had two files
equally named in two different paths.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16788 85f007b7-540e-0410-9357-904b9bb8a0f7
Prettyp: avoid useless "let module"

 As hinted by X. Clerc, a "let module" induces some runtime cost,
 so let's try to avoid them when possible.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16789 85f007b7-540e-0410-9357-904b9bb8a0f7
universes-buraliforti-redef.v : repair a match after Pierre B. syntax changes

 This file, which is currently expected to fail at the last line
 (with Universe Inconsistency), was actually failing earlier
 after Pierre Boutillier changed the patterns (parameters are required now).

 A final "Fail" will soon arrives here to avoid such issue in the future...

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16790 85f007b7-540e-0410-9357-904b9bb8a0f7
Uminus.v : prepare this test file for the use of Fail

 - Highlight the fact that the line defining "up" is the one which
   should fail.
 - Factor code with stdlib's Hurkens.v
 - This way, this test could become a "shouldnotfail" test by placing
   two final "Fail" (before the definitions of "up" and "paradox").

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16791 85f007b7-540e-0410-9357-904b9bb8a0f7
Use "Fail" rather than rely on exit code.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16792 85f007b7-540e-0410-9357-904b9bb8a0f7
Update test for bug 2846 in order to use "Fail".

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16793 85f007b7-540e-0410-9357-904b9bb8a0f7
Execute tests from the "bugs/closed" directory.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16794 85f007b7-540e-0410-9357-904b9bb8a0f7
Wrong bug identifier.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16795 85f007b7-540e-0410-9357-904b9bb8a0f7
Get rid of "shouldfail" subdirectory by moving tests to parent directory.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16796 85f007b7-540e-0410-9357-904b9bb8a0f7
Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7
Merge "inductive?.v" tests into a single "inductive.v" test.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16798 85f007b7-540e-0410-9357-904b9bb8a0f7
Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16799 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix name clash in "failure/inductive.v".

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16800 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing ocamldebug compilation by adding thread linking.

git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@16801 85f007b7-540e-0410-9357-904b9bb8a0f7