diff options
Diffstat (limited to 'src/Reflection/Eta.v')
| -rw-r--r-- | src/Reflection/Eta.v | 2 |
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. |