fix parsing of ---- +++++ ***** in CoqIDE
Taking into account factorization of consecutive names of same types
in goal context.

Note: printing of a declaration was previously done in the context
made of the preceding segment of hypotheses, while now it is made in
the full context of all hyps (those coming before and after the hyp
being printed). As a consequence, constants which could be confused
with a variable in the context are now always qualified even if the
conflicting variable name is coming later. But why not, that looks
somehow more uniform like this.
Fixing clash in output test-suite Cases.
Fixing order of declarations in the function which compacts variables
of same type in a context.
No hash consing across calls to the native compiler.

The induced side effects were incompatible with the undo machinery.
Fix typo in documentation of the [repeat] tactical.

Closes #3761.
-help failing (fix 3762)
Fix retroknowledge for int31 division.

Was broken accidentally by 5b0769b33, slowing down vm_compute and native_compute
on numeric computations.
Addressing report #3279 (inconsistency of behavior of the -> and <-
introduction patterns).

Whether we call -> and <- from assert as or apply in as, or as a
component of a larger introduction pattern, the new documented
semantics is:

- behave as subst if an equation rewriting a variable (rewrite in
  conclusion and hyps and erase variable and hyp).
- rewrite in concl if an equation not rewrite a variable or a
  quantified equality, then erase the hypothesis.

This is potential source of incompatibilities.
Fixing order of hypothesis in goal hypotheses compaction for coqtop.
Documenting some incompatibilities in (non) Import of ML tactics,
Apparently, the former refine was simplifying in hypotheses too.
Remove an ununsed pattern and commented code in the kernel.
Reestablish completeness in conversion when Opaque primitive
projections are used.
Change reduction_of_red_expr to return an e_reduction_function returning
an updated evar_map, as pattern is working up to universe equalities
that must be kept. Straightforward adaptation of the code depending on
this.
Fix generation of the index_urls.txt file.

Hevea has stopped producing HTML4 code two years ago. So the old sed
expression was producing an empty index file for any user with a
non-deprecated version of hevea.
Install index_urls.txt in a location where coqide might actually find it.
VarInstance are also goals.
This commit introduces changes in induction and destruct.

The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
  the "at" is given, of whether the subterm is fully applied or not,
  and whether there are incompatible subterms matching the pattern. In
  particular, we have:
  "at" given
  | subterm fully applied
  | | incompatible subterms
  | | |
  Y Y - it works like in 8.4
  Y N - this was broken in 8.4 ("at" was ineffective and it was finding
        all subterms syntactically equal to the first one which matches)
  N Y Y it now finds all subterms like the first one which matches
        while in 8.4 it used to fail (I hope it is not a too risky in-draft
        for a semantics we would regret...) (e.g. "destruct (S _)" on
        goal "S x = S y + S x" now selects the two occurrences of "S x"
        while it was failing before)
  N Y N it works like in 8.4
  N N - it works like in 8.4, selecting all subterms like the
        first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
  select all subterms that syntactically match the first subterm to
  match the pattern (looking from left to right) is now internally called
  "like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
  for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
  finding the subterm: it could be easily replaced by an other
  matching algorithm.

In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".

Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
  time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
  holes in c, we need the sigma obtained from c to be an extension of
  the sigma of the tactics, while before, we just type-checked c
  independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
  pending conversion problems) is made slightly cleaner: it now takes
  three states: a term is evaluated in state sigma, leading to state
  sigma' >= sigma, with evars finally solved in state sigma'' >=
  sigma'; we solve evars in the diff of sigma' and sigma and report
  the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
  when "c" has unresolved holes, waiting instead for a decision on
  what to do in the case of a similar eapply (see mail to coqdev).

An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.

Incidentally, make_abstraction does not do evar resolution itself any longer.
Changed implementation of lib/heap.ml to use Braun trees

The previous implementation was embarrassingly naive and inefficient.
For elements with the same priority, this new implementation may return
a maximum element that is different (yet still with the highest priority,
of course).
This code is used only in tactic firstorder.
Dead code + typo.