Trickyer test for Paral-ITP

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16740 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove Obj.magic from safe typing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16741 85f007b7-540e-0410-9357-904b9bb8a0f7
-coq-slaves: close_on_exec + correct argument passing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16742 85f007b7-540e-0410-9357-904b9bb8a0f7
Stm: if slave process dies badly go back to local lazy evaluation

Processing the proof in a slave process may fail for an implementation
error, e.g. the state could not be marshalled, or an anomaly is raised
by the slave.

In this case we fall back to local, lazy, evaluation in the master
process.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16743 85f007b7-540e-0410-9357-904b9bb8a0f7
safe Conv_oracle state for type checking

safe_typing is not purely functional, hence we cannot chain it
as if it was a pure computation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16744 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix typo in error message

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16745 85f007b7-540e-0410-9357-904b9bb8a0f7
recdef: restore old semantics (pre STM)

The Stm commit switched from an home made handling of failures to
a with_state_protection.  This was wrong, since in case of success
the global state has to be left altered.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 85f007b7-540e-0410-9357-904b9bb8a0f7
ind_tables: properly handling side effects

If a constant is defined as transparent, not only its side effects
(opaque sub proofs as in abstract, and transparent ind schemes)
are declared globally, but the ones that are schemes are also declared
as such.

The only sub optimal thing is that the code handling in a special
way the side effects of transparent constants is in declare.ml that
does not see ind_tables.ml, hence a forward ref to a function is used.
IMO, ind_tables has no reason to stay in toplevel/.

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