Preserving the good effect of 014e5ac92a on not leaving dangling local

definitions while keeping some compatibility on when to generalize
when an index also occur in a parameter (effect on PersistentUnionFind
for instance).

2 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 2aa07cde1b..56cdf18e68 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -396,6 +396,7 @@ Abort.
 Goal 2=1 -> 1=0.
 intro H. destruct H.
 Fail (match goal with n:nat |- _ => unfold n end). (* Check that no let-in remains *)
+Abort.
 
 (* Check clearing of names *)
 
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 0d0466cb58..3715f65f6c 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -140,3 +140,14 @@ intros x H1 H.
 induction H.
 change True in IHrepr'.
 Abort.
+
+(* In this case, generalization was done in 8.4 and we preserve it; this
+   is arbitrary choice  *)
+
+Inductive repr'' : nat -> nat -> Prop := reprc'' x z : repr'' x z -> repr'' x z.
+
+Goal forall x, 0 = x -> repr'' x x -> True.
+intros x H1 H.
+induction H.
+change (0 = z -> True) in IHrepr''.
+Abort.