Shortcuts and optimizations of comparisons

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15120 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing a few bugs (see #2571) related to interpretation of multiple binders
- fixing missing spaces in the format of the exists' notations (Logic.v);
- fixing wrong variable name in check_is_hole error message (topconstr.ml);
- interpret expressions with open binders such as "forall x y, t" as
  "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid
  the "implicit type" of a variable being propagated to the type of
  another variable of different base name.

An open question remains: when writing explicitly "forall (x y:_),t",
should the types of x and y be the same or not. To avoid the "bug"
that x and y have implicit types but the one of x takes precedences, I
enforced the interpretation (in constrintern, not in parsing) that
"forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However,
another choice could have been made. Then one would have to check that
if x and y have implicit types, they are the same; also, glob_constr
should ideally be changed to support a GProd and GLam with multiple
names in the same type, especially if this type is an evar. On the
contrary, one might also want e.g. "forall x y : list _, t" to mean
"forall (x:list _) (y:list _), t" with distinct instanciations of
"_" ...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7
Unifying the different procedures for interning binders.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15122 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing the "capture" check newly introduced in r15122 when
internalizing declaration of contexts of the form "(x y : P x)":
- don't forget to catch the error in intern_context;
- check capture on glob_constr rather than constr_expr so that binders
  possibly introduced by notations are recognized as such;
- give a more expressive error message.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15123 85f007b7-540e-0410-9357-904b9bb8a0f7
Added a background color configuration option in CoqIDE.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15127 85f007b7-540e-0410-9357-904b9bb8a0f7
Added a reset button for CoqIDE colors

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15128 85f007b7-540e-0410-9357-904b9bb8a0f7
remove plugins/subtac/subtac.ml reintroduced by mistaked in a previous commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15129 85f007b7-540e-0410-9357-904b9bb8a0f7
CHANGES: adapt after backport of some features to 8.4

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15131 85f007b7-540e-0410-9357-904b9bb8a0f7
lib directory is cut in 2 cma.

 - Clib that does not depend on camlpX and is made to be shared by all coq
   tools/scripts/...
 - Lib that is Coqtop specific

As a side effect for the build system :
 - Coq_config is in Clib and does not appears in makefiles
 - only the BEST version of coqc and coqmktop is made
 - ocamlbuild build system fails latter but is still broken

(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)

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

Bug 2736: Syntax highlighting

600 transitions left before ocamllex limit.

A preference pane large enough to change fonts.

Erase extra empty line in Coqide goal display.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15145 85f007b7-540e-0410-9357-904b9bb8a0f7
"A -> B" is a notation for "forall _ : A, B".

No good reason for that except uniformity so revert this commit if you find a
reason against it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15146 85f007b7-540e-0410-9357-904b9bb8a0f7
make otags only relies on otags

but it requires otags-3.12.2 and and ./configure -usecamlp4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15147 85f007b7-540e-0410-9357-904b9bb8a0f7
Remove print call that do not use the pp mechanism

Signed-off-by: Edward Z. Yang <ezyang@mit.edu>

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
Browser documentation  & CharSet under Windows

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
Removed syntax BeginSubproof/EndSubproof. It has been replaced by
braces ( { / } ).

BeginSuproof n (where n is a goal number) can be replaced by Focus n. { .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15158 85f007b7-540e-0410-9357-904b9bb8a0f7
Better error message when defining recursive records with Record or
Structure.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15159 85f007b7-540e-0410-9357-904b9bb8a0f7
Restores pdf bookmarks in the reference manual.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15160 85f007b7-540e-0410-9357-904b9bb8a0f7
Documentation of records defined with the keywords Inductive and
CoInductive.

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