diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-10 11:12:00 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-10 11:12:00 -0500 |
| commit | b5abd9004bcd60596424b2f55927d43ee6ea663c (patch) | |
| tree | 59aa503ffdedf136a7b7f27c58f9c72867cb28d5 /src | |
| parent | 2b3c61ff26eee88ba043954f6237ae1798f63e63 (diff) | |
Fix more unfolding
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/SmartMap.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Reflection/SmartMap.v b/src/Reflection/SmartMap.v index 7a710eb0b..5ab416355 100644 --- a/src/Reflection/SmartMap.v +++ b/src/Reflection/SmartMap.v @@ -172,7 +172,7 @@ Section homogenous_type. | Syntax.Tbase x => fv _ | Unit => fun v _ => v | Prod A B => fun (xy : interp_flat_type _ A * interp_flat_type _ B) - (x'y' : interp_flat_type _ _ * interp_flat_type _ B) + (x'y' : interp_flat_type _ A * interp_flat_type _ B) => (@SmartFlatTypeMapInterp2 _ _ _ f fv A (fst xy) (fst x'y'), @SmartFlatTypeMapInterp2 _ _ _ f fv B (snd xy) (snd x'y')) end. @@ -186,7 +186,7 @@ Section homogenous_type. | Syntax.Tbase x => fv _ | Unit => fun _ v => v | Prod A B => fun (v : interp_flat_type _ A * interp_flat_type _ B) - (xy : interp_flat_type _ _ * interp_flat_type _ _) + (xy : interp_flat_type _ (SmartFlatTypeMap _ (fst v)) * interp_flat_type _ (SmartFlatTypeMap _ (snd v))) => (@SmartFlatTypeMapUnInterp _ _ _ f fv A _ (fst xy), @SmartFlatTypeMapUnInterp _ _ _ f fv B _ (snd xy)) end. @@ -252,7 +252,7 @@ Section hetero_type. | Tbase x => fv _ | Unit => fun _ v => v | Prod A B => fun (v : interp_flat_type _ A * interp_flat_type _ B) - (xy : interp_flat_type _ _ * interp_flat_type _ _) + (xy : interp_flat_type _ (SmartFlatTypeMap2 _ (fst v)) * interp_flat_type _ (SmartFlatTypeMap2 _ (snd v))) => (@SmartFlatTypeMapUnInterp2 _ _ _ f fv A _ (fst xy), @SmartFlatTypeMapUnInterp2 _ _ _ f fv B _ (snd xy)) end. |