Implement the substitution function for global options. Fixes anomaly in ssreflect compilation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14991 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: correct compare_neq (fix #2703)

 The earlier version was a bit too quick to answer <= while strict
 constraints could still appear from remaining universes to explore.
 Typical situation: compare u v when u <= v and u <= w < v.
 Encountering u <= v isn't enough to conclude yet...

 This means that kernels from r13719 to now in trunk, and
 from r13735 to now in 8.3 (including 8.3pl{1,2,3}) couldn't accurately
 detect universe inconsistencies, leading to potential proofs of False!
 Oups, sorry...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14993 85f007b7-540e-0410-9357-904b9bb8a0f7
Coq_makefile: Add of extra options by default

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14997 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug 2703: send stdout dump to coqide when an error occurs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14998 85f007b7-540e-0410-9357-904b9bb8a0f7
Vector: missing injection lemmas and better impossible branches

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14999 85f007b7-540e-0410-9357-904b9bb8a0f7
In the syntax of pattern matching, "in" clauses are patterns.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15000 85f007b7-540e-0410-9357-904b9bb8a0f7
In the syntax of pattern matching, the arguments of the inductive in the "in"
clause can be any pattern.

It is expanded as a match in the return clause.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15001 85f007b7-540e-0410-9357-904b9bb8a0f7
RefMan update about match syntax.

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

I love being push under presure to commit and do not try my fixup !

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15004 85f007b7-540e-0410-9357-904b9bb8a0f7
correcting a little bug in invfun.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15005 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: a faster is_leq test used when possible

 Let's reintroduce the idea of stopping the graph traversal as
 soon as a LE arc has been found, but this time we do so only
 when we're not interested by the LT/LE distinction.

 This way, we should remain correct but avoid largly the time penalty
 induced by the last fix on univ.ml: the +30% on contrib Container
 is almost gone, let's hope it'll be the same with Ssreflect.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15007 85f007b7-540e-0410-9357-904b9bb8a0f7
various corrections in invfun due to a modification in induction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15008 85f007b7-540e-0410-9357-904b9bb8a0f7
New version of recdef :
 + Allowing much more function to be defined.
 + Using completely new algorithm to define non structural fixpoints

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15009 85f007b7-540e-0410-9357-904b9bb8a0f7
Removed a superfluous function in proof.mli. Preparing for incoming
changes of the handling of unfocusing errors.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15010 85f007b7-540e-0410-9357-904b9bb8a0f7
Corrects the erroneous error message when trying to unfocus a fully
unfocused proof (part of bug #2671).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15011 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: a better Constraint.compare

Let's gain a few % by not using Pervasive.compare on a structure containing
some universe_levels, but rather UniverseLevel.compare on them.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15012 85f007b7-540e-0410-9357-904b9bb8a0f7
Univ: a univ_depends function to avoid a hack in Inductiveops

 univ_depends checks whether a universe variable appears or
 is equal to a universe. In comparison with the previous hack
 in inductiveops based on try...catching UniverseInconsistency,
 this should be semantically equivalent, simplier, and more
 robust in case we allow someday an unsafe mode where
 merge_constraints would be a no-op.

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

Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.

+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
"Let in" in pattern hell, one more iteration

This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf.

An other wrong externalize function

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