Coqmktop: use the atomic Filename.open_temp_file

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16016 85f007b7-540e-0410-9357-904b9bb8a0f7
Identities over types satisfying Uniqueness of Identity Proofs
themselves satisfied Uniqueness of Identity Proofs. Otherwise said
uniqueness of equality proofs is enough to characterize types whose
equality has a degenerated "homotopical" structure (this is a short
proof of a result inspired by Voevodsky's proof of inclusion of
h-level n into h-level n+1).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16017 85f007b7-540e-0410-9357-904b9bb8a0f7
Display Menu now called View Menu (in CoqIDE preferences).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16018 85f007b7-540e-0410-9357-904b9bb8a0f7
Revised the strategy for automatic insertion of spaces when printing
notations: - hopefully never 2 spaces when the user did not ask for -
more systematic default insertion of spaces around symbols - e.g. have
space before "[" if after a non-terminal - have spaces between
consecutive terminals

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16020 85f007b7-540e-0410-9357-904b9bb8a0f7
Low-level hack to get some more informative message from dynamic loading errors.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16021 85f007b7-540e-0410-9357-904b9bb8a0f7
Early translation of camlp4/camlp5 located errors into coq-located
errors so as to be able to work only with Loc.Exc_located inside main
Coq. This fixes the anomaly (probably introduced by commit 15847) when
a syntax error arrives in coqc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16022 85f007b7-540e-0410-9357-904b9bb8a0f7
Removed Compat.Exc_located outside of compat.ml4, as a consequence of
previous commit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16023 85f007b7-540e-0410-9357-904b9bb8a0f7
Backtrack on activating scopes with type casts (was r15978).

IT happens that there are some other uses of casts, e.g. in nat_int de
MathClasses which uses a notation 0 for some class constructor zero,
and a cast (0:nat) to force this notation 0 to represent the instance
O in nat of the class of types having a zero (eventually, 0,
i.e. "zero nat O" and "O" are convertible but the information of being
a class instance is lost).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16024 85f007b7-540e-0410-9357-904b9bb8a0f7
Making subset_eq_compat applying over more general domain "Type" (see #2938).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16025 85f007b7-540e-0410-9357-904b9bb8a0f7
Restoring flush of Welcome message lost in r15148

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16026 85f007b7-540e-0410-9357-904b9bb8a0f7
* tools/Coq_makefile:
  Add '-I config' in the options of the ocaml compilers.
  This is useful to reuse site configuration in plugins.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16027 85f007b7-540e-0410-9357-904b9bb8a0f7
* tools/Coq_makefile
  Export $(COQMKTOP) in generated Makefiles.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16028 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "* tools/Coq_makefile:"

This reverts commit 9a2f43eca179436f0581751b93c989fd30a5c13c.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16029 85f007b7-540e-0410-9357-904b9bb8a0f7
* lib/Envars:
  - Document interface file.
  - Now export references to ocaml compilers used to compile Coq.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implementing the "union by rank" optimisation in univ.ml
* Bugfixes in union by rank in univ.ml
kernel/univ.ml: clarify the rank union selection logic