diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-20 17:54:12 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-20 17:54:12 -0400 |
| commit | 6d1b72933ad4e718cf463bcec495aea95828a5ff (patch) | |
| tree | f36106c04564c66f37c37f4ed2c1383677afc8ae /src/Compilers/InlineConstAndOp.v | |
| parent | 73ad66772245abf3ae65721de589ed2bd6de7505 (diff) | |
Better typing on postprocess_for_const_and_op
Diffstat (limited to 'src/Compilers/InlineConstAndOp.v')
| -rw-r--r-- | src/Compilers/InlineConstAndOp.v | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/src/Compilers/InlineConstAndOp.v b/src/Compilers/InlineConstAndOp.v index dce6d5359..842fc628a 100644 --- a/src/Compilers/InlineConstAndOp.v +++ b/src/Compilers/InlineConstAndOp.v @@ -49,7 +49,9 @@ Section language. | partial_inline tx tC ex eC, partial_inline ty tC' ey eC' => fun _ => partial_inline (tC:=Prod _ _) - (Pair ex ey) (fun '(x, y) => (eC x, eC' y)) + (Pair ex ey) + (fun xy : interp_flat_type _ _ * interp_flat_type _ _ + => (eC (fst xy), eC' (snd xy))) | no_inline _ ex, no_inline _ ey => fun _ => no_inline (Pair ex ey) | no_inline tx ex, inline ty ey @@ -71,11 +73,15 @@ Section language. | partial_inline tx tC ex eC, no_inline ty ey => fun _ => partial_inline (tC:=Prod _ _) - (Pair ex ey) (fun '(x, y) => (eC x, SmartVarVarf y)) + (Pair ex ey) + (fun xy : interp_flat_type _ _ * interp_flat_type _ _ + => (eC (fst xy), SmartVarVarf (snd xy))) | no_inline tx ex, partial_inline ty tC ey eC => fun _ => partial_inline (tC:=Prod _ _) - (Pair ex ey) (fun '(x, y) => (SmartVarVarf x, eC y)) + (Pair ex ey) + (fun xy : interp_flat_type _ _ * interp_flat_type _ _ + => (SmartVarVarf (fst xy), eC (snd xy))) | default_inline _ ex, default_inline _ ey => fun d => d | default_inline _ _, _ |