Also do eta under lets in Reflection/Eta.v

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Reflection/Eta.v b/src/Reflection/Eta.v
index 6a15ce60e..eda74f4a5 100644
--- a/src/Reflection/Eta.v
+++ b/src/Reflection/Eta.v
@@ -38,7 +38,7 @@ Section language.
            | Op t1 tR opc args => Op opc (@exprf_eta_gen _ args)
            | LetIn tx ex tC eC
              => LetIn (@exprf_eta_gen _ ex)
-                      (interp_flat_type_eta_gen eC)
+                      (interp_flat_type_eta_gen (fun x => @exprf_eta_gen _ (eC x)))
            | Pair tx ex ty ey => Pair (@exprf_eta_gen _ ex) (@exprf_eta_gen _ ey)
            end.
     End gen_flat_type.