Little oversight in commit r16489 (fix for bug #3036).

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16507 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing a source of evars leak, revealed by contrib QuicksortComplexity
after r16499 which replaced a check for visible undefined evars
(check_evars) by a check for undefined evars in the evar map
(check_evars_are_solved).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16508 85f007b7-540e-0410-9357-904b9bb8a0f7
Added a generic notion of hook. Hooks are functions to be set
exactly once at runtime, often to reduce the mutual dependency of
modules. This module permits to track them more easily.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
Use the Hook module here and there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing Gmap from Extraction plugin

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16511 85f007b7-540e-0410-9357-904b9bb8a0f7
Granting wish #3014:
  Hint Rewrite should allow multiple databases.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16513 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing the use of Fset/Fmap from Trie. There was actually only
one place depending on fold order, which was easy to bypass.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16514 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing Fset, since it is not used anymore.

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