diff options
author | 2014-11-02 22:13:27 +0100 | |
---|---|---|
committer | 2014-11-02 22:15:41 +0100 | |
commit | 4df1ddc6d6bd0707396337869b663b4c8f930f60 (patch) | |
tree | 6bbc012b84c3b7a6390f2096fbcfa21c5c357e36 /plugins | |
parent | bddc12b5f8706882bd870445891351b2cd8e8156 (diff) |
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).
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions