diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-03-10 11:06:52 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-03-10 11:06:52 -0500 |
| commit | 2b3c61ff26eee88ba043954f6237ae1798f63e63 (patch) | |
| tree | 2c8bc1b728e5edd7a081f16b5e1c7d460b7135d5 /src/Reflection/Relations.v | |
| parent | e4921f400fc64522541471853c630bebb17c158f (diff) | |
Fix more unfolding that shouldn't happen
Diffstat (limited to 'src/Reflection/Relations.v')
| -rw-r--r-- | src/Reflection/Relations.v | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v index 160d76b56..f7fbe682c 100644 --- a/src/Reflection/Relations.v +++ b/src/Reflection/Relations.v @@ -40,8 +40,9 @@ Section language. match t with | Tbase t => R t | Unit => fun _ => True - | Prod _ _ => fun x => and (interp_flat_type_rel_pointwise1_gen_Prop _ (fst x)) - (interp_flat_type_rel_pointwise1_gen_Prop _ (snd x)) + | Prod A B => fun x : interp_flat_type _ A * interp_flat_type _ B + => and (interp_flat_type_rel_pointwise1_gen_Prop _ (fst x)) + (interp_flat_type_rel_pointwise1_gen_Prop _ (snd x)) end. End pointwise1. Section pointwise2. @@ -51,8 +52,11 @@ Section language. match t with | Tbase t => R t | Unit => fun _ _ => True - | Prod _ _ => fun x y => and (interp_flat_type_rel_pointwise_gen_Prop _ (fst x) (fst y)) - (interp_flat_type_rel_pointwise_gen_Prop _ (snd x) (snd y)) + | Prod A B + => fun (x : interp_flat_type _ A * interp_flat_type _ B) + (y : interp_flat_type _ A * interp_flat_type _ B) + => and (interp_flat_type_rel_pointwise_gen_Prop _ (fst x) (fst y)) + (interp_flat_type_rel_pointwise_gen_Prop _ (snd x) (snd y)) end. End pointwise2. Section pointwise2_hetero. @@ -63,8 +67,9 @@ Section language. | Tbase t1, Tbase t2 => R t1 t2 | Unit, Unit => fun _ _ => True | Prod x1 y1, Prod x2 y2 - => fun a b => and (interp_flat_type_rel_pointwise_hetero_gen_Prop x1 x2 (fst a) (fst b)) - (interp_flat_type_rel_pointwise_hetero_gen_Prop y1 y2 (snd a) (snd b)) + => fun (a b : interp_flat_type _ _ * interp_flat_type _ _) + => and (interp_flat_type_rel_pointwise_hetero_gen_Prop x1 x2 (fst a) (fst b)) + (interp_flat_type_rel_pointwise_hetero_gen_Prop y1 y2 (snd a) (snd b)) | Tbase _, _ | Unit, _ | Prod _ _, _ |