From 4b075af747f65bcd73ff1c78417cf77edf6fbd76 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Jan 2016 01:13:56 +0100
Subject: 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.
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index a9fbfe29d0..cda16d3804 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,10 @@ Tactics
 - Flag "Bracketing Last Introduction Pattern" is now on by default.
 - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
   tactical w.r.t. variables appearing in the body of the proof.
+- Serious bugs are fixed in tactic "double induction" (source of
+  incompatibilities as soon as the inductive types have dependencies in
+  the type of their constructors; "double induction" remains however
+  deprecated).
 
 Program
 
-- 
cgit v1.2.3