2 files changed, 24 insertions, 0 deletions
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 14dc16072b..be1bff48ba 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -36,3 +36,13 @@ fun (A : Type) (x : I A) => match x with
 Argument scopes are [type_scope _]
 foo' = if A 0 then true else false
      : bool
+f = 
+fun H : B =>
+match H with
+| AC x =>
+    (let b0 := b in
+     if b0 as b return (P b -> True)
+     then fun _ : P true => Logic.I
+     else fun _ : P false => Logic.I) x
+end
+     : B -> True
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 505418b14c..30ef8778d3 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -58,3 +58,17 @@ Definition foo' :=
 
 Print foo'.
 
+(* Was bug #3293 (eta-expansion at "match" printing time was failing because
+   of let-in's interpreted as being part of the expansion)  *)
+
+Variable b : bool.
+Variable P : bool -> Prop.
+Inductive B : Prop := AC : P b -> B.
+Definition f : B -> True.
+
+Proof.
+intros [].
+destruct b as [|] ; intros _ ; exact Logic.I.
+Defined.
+
+Print f.