From e5a5fdb9ad8d57b37729a781b217701ac341f522 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Dec 2020 10:22:54 +0100
Subject: Add a test for cbv over inductive types which feature let-bindings.

---
 test-suite/success/cbv_let.v | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 test-suite/success/cbv_let.v

diff --git a/test-suite/success/cbv_let.v b/test-suite/success/cbv_let.v
new file mode 100644
index 0000000000..861a73a64e
--- /dev/null
+++ b/test-suite/success/cbv_let.v
@@ -0,0 +1,34 @@
+Record T : Type := Build_T { f : unit; g := pair f f; }.
+
+Definition t : T := {| f := tt; |}.
+
+Goal match t return unit with Build_T f g => f end = tt.
+Proof.
+cbv.
+reflexivity.
+Qed.
+
+Goal match t return prod unit unit with Build_T f g => g end = pair tt tt.
+Proof.
+cbv.
+reflexivity.
+Qed.
+
+Goal forall (x : T),
+  match x return prod unit unit with Build_T f g => g end =
+  pair match x return unit with Build_T f g => fst g end match x return unit with Build_T f g => snd g end.
+Proof.
+cbv.
+destruct x.
+reflexivity.
+Qed.
+
+Record U : Type := Build_U { h := tt }.
+
+Definition u : U := Build_U.
+
+Goal match u with Build_U h => h end = tt.
+Proof.
+cbv.
+reflexivity.
+Qed.
-- 
cgit v1.2.3