Fixing some problems with double induction.

Basically, the hypotheses were treated in an incorrect order, with a
hack for sometimes put them again in the right order, resulting in
failures and redundant hypotheses.

Status unclear, because this new version is incompatible except in
simple cases like a double induction on two "nat".

Fixing the bug incidentally simplify the code, relying on the
deprecation since 8.4 to allow not to ensure a compatibility (beyond
the simple situation of a double induction on simple datatypes).

See file induct.v for effect of changes.

0 files changed, 0 insertions, 0 deletions