Dead code + typo.
Fixing destruct/induction with a using clause on a non-inductive type,
that was broken by commit bf01856940 + use types from induction scheme
to restrict selection of pattern + accept matching from partially
applied term when using "using".
Applying like-first selection for destruct in hypotheses.
Preventing potential evar leak in Rewrite.
Fix some typos in comments.
Dead code
Fixing clash in test destruct.v.
Fixing evars lost in interpretation of eliminator of destruct.
Ensuring compatibility when an hypothesis used for destruct is
dependent in the goal without being fully applied: it cannot be
erased. This used to work in 8.4 when the hypothesis was in an empty
type. I fixed this and (somehow arbitrarily) generalized the
non-erasing to other inductive types instead of failing.
Making destruct on idents with maximal implicit arguments working, by
keeping them as open holes. When these arguments are class instances,
this restores compatibility with the 8.4 search for subterms from
non-fully applied patterns which was using conversion on the
instances.
Use the url package, since coqdoc generates \url commands.
Fix some typos.
Make sure that Logic/ExtensionalityFacts gets compiled.
Fixes for PG (Close 3763, 3770)

- Show does not print the goal twice
- Undo is considered as part of the document when PG mode
  (bug introduced when Undo was said not to be part of the document in
   coqtop mode).