Revert "Naming main goal "Main""

(More thinking needed)
In convert_concl/convert_hyp: nf_enter -> enter.
(Maybe one of the source of inefficiency introduced on Oct 9 - see e.g. CoLoR.)
Relaxing again the test on types of replacements in tactic change
(continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc).

It may be the case that the new expression lives in a higher sorts and
the context where it is substituted in supports it. So, it is too
strong to expect that, when the substituted objects are types, the
sort of the new one is smaller than the sort of the original
one. Consider e.g.

  Goal @eq Type nat nat.
  change nat with (@id Type nat).

which is a correct replacement, even if (id Type nat) is in a higher sort.

Introducing typing in "contextually" would be a big change for a
little numbers of uses, so we instead (hackily) recheck the whole term
(even though typing with evars uses evar_conv which accept to unify
Type with Set, leading to wrongly accept "Goal @eq Set nat nat.
change nat with (@id Type nat).". Evar conv is however rejecting
Prop=Type.)
More fallout from elisp rename

Commit 3e972b3ff8e532be233f70567c87512324c99b4e renamed coq.el,
coq-db.el, coq-syntax.el to gallina.el, gallina-db.el,
gallina-syntax.el without fixing up any of the references.  Commit
30b58d43e48569afb50a35d3915ec7d453a61f5d only fixed up some of them.
Here are some more (hopefully all of them).

Signed-off-by: Anders Kaseorg <andersk@mit.edu>