remove trailing '\r' from file names returned by coqtop
Uses slashes for install and config directories
Lets coqtop use a slash
make install-coqlight installs DLLCOQRUN and LIBCOQRUN
Inductive maps in Environ now use HMap.
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).