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>
Essai où assert_style n'est utilisé que si pas visuellement une équation;
Fixing a loop in proof reconstruction for congruence (#2447).

Proofs of C t1..tn+1 = C t1..tn+1, even when the terms were
syntactically the same, were built by composition of a proof of C
t1..tn = C t1..tn with a proof of reflexivity of tn+1. The latter was
reduced to showing C t1..tn = C u1..un for C u1..un the canonical
representant of C t1..tn in its congruence class. But if some pair
ti=ui was derivable by injectivity of the constructor C, it might go
back to find a proof of C t1..tn+1 = C t1..tn+1 again, while a simple
reflexivity proof was enough here.

Not sure that the fix prevents any further loop in this part of the
code though.
Re-displaying evar instances in debugger.
New experimental heuristic printing strategy for evar instances: We
don't print bindings of the form "x:=x" unless there is also a binding
"x':=x". Otherwise said, if a variable occurs several time, the
binding where it occurs under the form "x:=x" is printed anyway.  This
should help to understand where the instance is non trivial while
still not obfuscating display in goals with very long list of
uninteresting trivial instances.
Experimental printing of the signature of open evars in Check.
When facing problem ?id = ?id' in resolution of return predicate,
early call the standard resolution function which e.g. does
restriction and maybe solve the problem if pattern-like, instead of
postponing the problem.
Now printing "now a keyword" only in verbose mode.
Revert "Essai où assert_style n'est utilisé que si pas visuellement une équation;" which was committed by mistake.

This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
Revert "Fixing a loop in proof reconstruction for congruence (#2447)."
committed by mistake. The message pretended to have a fix which is only
superficially a fix. The problem is more complex.

This reverts commit 251218905daea0838a3738466afa1c278bb3e81b.
Fixing a bug in the presence of let-in in inductive arity.
A patch for printing "match" when constructors are defined with let-in
but the internal representation dropped let-in.

Ideally, the internal representation of the "match" should use
contexts for the predicate and the branches. This would however be a
rather significant change. In the meantime, just a hack.

To do, there is still an extra @ in the constructor name that does not
need to be there.
Fixing a (new) part of bug #2729.

By moving convert_concl to new proof engine, re-typecheckeing was
incidentally introduced. Re-typechecking revealed that vm bug #2729
was still open. Indeed, the vm was still producing an ill-typed term.

This commit fixes ill-typedness of the vm in #2729 when reconstructing
a "match" in an inductive type whose constructors have let-ins.

Another part is still open (see test-suite).
Removing re-typecheking from "refine" in no-check mode of the new
convert_concl/convert_hyp. This was actually probably the main source
of inefficiency introduced on Oct 9 (see e.g. CoLoR), rather than
nf_enter, as suspected in 3c2723f.
Continuing experimental printing of the signature of open evars in
Check (see cfff8f8a327) [printing only visible evars, not the ones
corresponding to unrelated open goals + fixing bug on wrong sigma and
on evar_info normalization].
Dead code.
More precise test for #3459.