Fixing injection in the presence of let-in in constructors.

This also fixes decide equality, discriminate, ... (see e.g. #5279).

2 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index a759674115..6abfca4c3f 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -38,3 +38,10 @@ Abort.
 Goal ~ identity 0 1.
 discriminate.
 Qed.
+
+(* Check discriminate on types with local definitions *)
+
+Inductive A := B (T := unit) (x y : bool) (z := x).
+Goal forall x y, B x true = B y false -> False.
+discriminate.
+Qed.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index da2183841d..78652fb64b 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -150,6 +150,13 @@ match goal with
 end.
 Abort.
 
+(* Injection in the presence of local definitions *)
+Inductive A := B (T := unit) (x y : bool) (z := x).
+Goal forall x y x' y', B x y = B x' y' -> y = y'.
+intros * [= H1 H2].
+exact H2.
+Qed.
+
 (* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.