diff options
Diffstat (limited to 'theories/Setoids')
| -rw-r--r-- | theories/Setoids/Setoid.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 9496099a8..884f05e52 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -339,7 +339,7 @@ with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Typ Definition product_of_arguments : Arguments -> Type. induction 1. exact (carrier_of_relation_class a). - exact (prodT (carrier_of_relation_class a) IHX). + exact (prod (carrier_of_relation_class a) IHX). Defined. Definition get_rewrite_direction: rewrite_direction -> Argument_Class -> rewrite_direction. |