fix batch compilation of scripts containing Admitted

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16689 85f007b7-540e-0410-9357-904b9bb8a0f7
checker validation made a bit more verbose

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16690 85f007b7-540e-0410-9357-904b9bb8a0f7
checker validation fixed w.r.t. Futures

still not working, it complains about the universe constraint
set...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16691 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix batch compilation of scripts with Admitted proofs (in a section)

This time all collateral effects of forcing the execution
of dropped proofs should be handled correctly

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16692 85f007b7-540e-0410-9357-904b9bb8a0f7
Adding the processed tag to comments in CoqIDE.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16693 85f007b7-540e-0410-9357-904b9bb8a0f7
Lemmas ending with Defined cannot be delegated to slaves

We need the proof object to continue (there is no real dependency
tracking so we assume we need it immediately).

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16695 85f007b7-540e-0410-9357-904b9bb8a0f7
Printing any backtrace in debug mode, not only anomalies.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16696 85f007b7-540e-0410-9357-904b9bb8a0f7
Mutual proofs cannot be delegated

I don't know why yet, but let's be conservative

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16697 85f007b7-540e-0410-9357-904b9bb8a0f7
Automatic backtracking if locked zone is edited

That is pretty tricky, and is not as nice I would like
for to_process text (that is still considered as locked).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16698 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing potentially misused Errors.push.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16700 85f007b7-540e-0410-9357-904b9bb8a0f7
Tooltips can be augmented with custom widgets, still not clickable

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16701 85f007b7-540e-0410-9357-904b9bb8a0f7
abstract+Defined: create opaque sub proofs (as pre-ParalITP)

Non-opaque-constant's side effects are processed before
the constant enters the kernel and global constants are
generated for them (as before, but not by side effect in
the middle of the proof construction).
This makes sense because proofs ending with Defined have
to be run immediately, so the list of side effects is
immediately available.

These side effects are type checked again.
To fix that the idea of kernel signatures could be employed.

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

No semantic change, but way less debug printings
coming from Paral-ITP

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16703 85f007b7-540e-0410-9357-904b9bb8a0f7
Modulification and removing of structural equality in VCS.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16704 85f007b7-540e-0410-9357-904b9bb8a0f7
Modulification and removing of structural equality in Stateid.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
Repair coqcheck : constant_body constraints are also future

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16706 85f007b7-540e-0410-9357-904b9bb8a0f7
Attempt to restore hash-consing of opaque terms

 Without this, the stdlib vo files are +30% larger

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

 - No more modinfo sub-record in the safe_environment record,
   this was a syntactic pain.
     senv.modinfo.modpath --> senv.modpath
     senv.modinfo.variant --> senv.modvariant
     senv.modinfo.resolver --> senv.modresolver
     senv.modinfo.resolver_of_param --> senv.paramresolver
     senv.modinfo.label : removed (can be inferred from modpath)

 - No more systematic chaining of safe_environment ('old' field).
   Instead, earlier safe_environment is stored in the modvariant field
   when necessary (STRUCT and SIG case).

 - Improved sharing between end_module and end_modtype

 - More qualified names instead of open, better comments, ...

 - Some user errors are now checked earlier elsewhere (see for
   instance vernac_end_segment), so we can turn these errors into
   asserts. The user error about higher-order include is now algebraic.

 - Highlight the idea of a state monad in Safe_typing :
   type 'a safe_transformer = safe_environment -> 'a * safe_environment
   More systematic code in Global, thanks to 'globalize' function.

 - Declaremods : less informations stored in openmod_info

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