diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-10 16:07:24 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-10 16:07:24 -0500 |
| commit | 5a21585b11d2e10dbaee28e9a48c86f3c41ff21b (patch) | |
| tree | 7914dd1ff84e52c8ced1179c631326caccf7766a /src/Reflection/BoundByCast.v | |
| parent | 7aac6f3d870e0952def2d9d8eeb391e2ea3785f7 (diff) | |
Use Eta in BoundByCast
Diffstat (limited to 'src/Reflection/BoundByCast.v')
| -rw-r--r-- | src/Reflection/BoundByCast.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/src/Reflection/BoundByCast.v b/src/Reflection/BoundByCast.v index 9b15e3724..fc2e6d11c 100644 --- a/src/Reflection/BoundByCast.v +++ b/src/Reflection/BoundByCast.v @@ -5,6 +5,7 @@ Require Import Crypto.Reflection.SmartMap. Require Import Crypto.Reflection.Inline. Require Import Crypto.Reflection.Linearize. Require Import Crypto.Reflection.MapCast. +Require Import Crypto.Reflection.Eta. Require Import Crypto.Util.Notations. Local Open Scope expr_scope. @@ -253,15 +254,16 @@ Section language. Definition Boundify {t1} (e1 : Expr t1) args2 : Expr _ - := InlineConstGen - (@push_cast) - (Linearize - (SmartBound - (@MapInterpCast - base_type_code interp_base_type_bounds - op (@interp_op_bounds) - (@failf) - (@bound_op) - t1 e1 (interp_all_binders_for_to' args2)) - (interp_all_binders_for_to' args2))). + := ExprEta + (InlineConstGen + (@push_cast) + (Linearize + (SmartBound + (@MapInterpCast + base_type_code interp_base_type_bounds + op (@interp_op_bounds) + (@failf) + (@bound_op) + t1 e1 (interp_all_binders_for_to' args2)) + (interp_all_binders_for_to' args2)))). End language. |