From 4f2bbf0c82f8ea4ba26990770fb1f103a6ca1668 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Nov 2014 12:36:30 +0100
Subject: Compatibility with 8.4 in the heuristic used to build the induction
 hypothesis when indices also occur among parameters. This solves current
 failure of PersistentUnionFind.

---
 test-suite/success/induct.v | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 4b0b5d01c1..0d0466cb58 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -113,3 +113,30 @@ induction x as [|n IHn].
 2:change (n = 0) in IHn. (* We don't want a generalization over cond *)
 Abort.
 End S3.
+
+(* These examples show somehow arbitrary choices of generalization wrt
+   to indices, when those indices are not linear. We check here 8.4
+   compatibility: when an index is a subterm of a parameter of the
+   inductive type, it is not generalized. *)
+
+Inductive repr (x:nat) : nat -> Prop := reprc z : repr x z -> repr x z.
+
+Goal forall x, 0 = x -> repr x x -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr.
+Abort.
+
+Goal forall x, 0 = S x -> repr (S x) (S x) -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr.
+Abort.
+
+Inductive repr' (x:nat) : nat -> Prop := reprc' z : repr' x (S z) -> repr' x z.
+
+Goal forall x, 0 = x -> repr' x x -> True.
+intros x H1 H.
+induction H.
+change True in IHrepr'.
+Abort.
-- 
cgit v1.2.3