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.