diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-07 19:46:17 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-07 19:46:17 -0500 |
| commit | 929d223e9d212eb0f0a98c14ee5a84f599474e2f (patch) | |
| tree | 31356f8ac536a8e224f1a22e23f60cd005c05125 /src/Reflection/Relations.v | |
| parent | d9d216d87eebc1b9c16932795ad2e56808a77e22 (diff) | |
Fix relation relb arguments
Diffstat (limited to 'src/Reflection/Relations.v')
| -rw-r--r-- | src/Reflection/Relations.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v index 8542415c6..a7f7bf7fc 100644 --- a/src/Reflection/Relations.v +++ b/src/Reflection/Relations.v @@ -319,7 +319,10 @@ Global Arguments interp_type_gen_rel_pointwise2 {_ _ _} R {t} _ _. Global Arguments interp_flat_type_rel_pointwise_gen_Prop {_ _ _ P} and True R {t} _ _. Global Arguments interp_flat_type_rel_pointwise_hetero_gen_Prop {_ _ _ P} and True False R {t1 t2} _ _. Global Arguments interp_flat_type_rel_pointwise_hetero {_ _ _} R {t1 t2} _ _. +Global Arguments interp_flat_type_relb_pointwise_hetero {_ _ _} R {t1 t2} _ _. Global Arguments interp_flat_type_rel_pointwise1 {_ _} R {t} _. +Global Arguments interp_flat_type_relb_pointwise1 {_ _} R {t} _. Global Arguments interp_flat_type_rel_pointwise {_ _ _} R {t} _ _. +Global Arguments interp_flat_type_relb_pointwise {_ _ _} R {t} _ _. Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _. Global Arguments interp_type_gen_rel_pointwise {_ _} _ {_} _ _. |