Some reorganization of the code for destruct/induction:

- It removes some redundancies.
- It fixes failures when destructing a term mentioning goal hypotheses
  x1, ..., xn or a term which is a section variable x when this term
  is in a type with indices, and the indices also occur in the type of
  one of x1, ..., xn, or of x.
- It fixes non-respect of eliminator type when completing pattern possibly
  given by a prefix.
- It fixes b2e1d4ea930c which was dealing with the case when the term
  was a section variable (it was unfortunately also breaking some
  compatibility about which variables variable were generalized in
  induction and which variables were automatically cleared because
  unselected).

0 files changed, 0 insertions, 0 deletions