From 23ad67d5e219f557a32ed6b77a2d961a52b10c92 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Tue, 10 Dec 2019 10:02:49 +0100
Subject: Fixing #9893 (Letins not supported in the specialized hypothesis).

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

(limited to 'test-suite')

diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index f12db8b081..1b04594290 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -109,6 +109,28 @@ match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
 
+(* let ins should be supported in the type of the specialized hypothesis *)
+Axiom foo: forall (m1 m2: nat), let n := 2 * m1 in m1 = m2 -> False.
+Goal False.
+  pose proof foo as P.
+  assert (2 = 2) as A by reflexivity.
+  specialize P with (1 := A).
+  assumption.
+Qed.
+
+(* Another more subtle test on letins: they should not interfere with foralls. *)
+Goal forall (P: forall y:nat,
+                forall A (zz:A),
+                  let a := zz in
+                  let x := 1 in
+                  forall n : y = x,
+                    n = n),
+    True.
+  intros P.
+  specialize P with (zz := @eq_refl _ 2).
+  constructor.
+Qed.
+
 (* Test specialize as *)
 
 Goal (forall x, x=0) -> 1=0.
-- 
cgit v1.2.3