Fixing generic equality in Auto.
Fix lookup of native files when option -R is missing.

Testcase:
mkdir a
echo "Definition t := O." > a/a.v
coqc -R a a a/a.v
echo "Require Import a.a. Definition u := t." > b.v
coqc -I . b.v
rm -rf a b.*
Compiling coqc in "tools" target.
Tentative fix for a very strange pervasive equality in Auto.
Using Hashmaps by default in constant and inductive maps. This changes fold and
iter order, but it seems nobody was relying on it (contrarily to the string case).
Useless tactic bindings in Tacticals.
Potentially unused computation in Goal.
Also use HMaps in KNmap.
Using HMaps in global references.
Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.
MaybeFlexible semantic changes

From Maybe reducible to Maybe to reduce (but for sure reducible)
Evarconv unification respects Conv_oracle
Useless Array.to_list in Typeops.
Fix (3243): univ constraints of module subtyping were not propagated

Universe constraints coming from subtyping were not propagated
to the outermost module and hence not stocked in the .vo file.
Still, they were added to the interactive safe environment and
hence checked for satisfiability.
vi2vo: universes handling finally fixed

Universes that are computed in the vi2vo step are not part of the
outermost module stocked in the vo file.  They are part of the
Library.seg_univ segment and are hence added to the safe env when
the vo file is loaded.

The seg_univ has been augmented.  It is now:
- an array of universe constraints, one for each constant whose opaque
  body was computed in the vi2vo phase.  This is useful only to print
  the constants (and its associated constraints).
- a union of all the constraints that come from proofs generated in the
  vi2vo phase.  This is morally the missing bits in the toplevel module
  body stocked in the vo file, and is there to ease the loading of
  a .vo file (obtained from a .vi file).
- a boolean, false if the file is incomplete (.vi) and true if it is
  complete (.vo obtained via vi2vo).
CoqIDE: detachable message/error/jobs panes
CoqIDE: Errors page gets red if not empty
Stm: smarter delegation policy

Stm used to delegate every proof when it was possible, but this may
be a bad idea.  Small proofs may take less time than the overhead
delegation implies (marshalling, etc...).

Now it delegates only proofs that take >= 1 second.

By default a proof takes 1 second (that may be wrong).

If the file was compiled before, it reuses the data stored in the .aux
file and assumes the timings are still valid.

After a proof is checked, Coq knows how long it takes for real, so it
wont predict it wrong again (when the user goes up and down in the
file for example).

CoqIDE now sends to Coq, as part of the init message, the file name
so that Coq can load the .aux file.
fake_ide: fix compilation
STM: move out a couple of submodules

These modules are not as reusable as one may want them to be, but
moving them out simplifies a little STM.