diff options
Diffstat (limited to 'theories/Setoids')
| -rw-r--r-- | theories/Setoids/Setoid.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index e09c3bc84..3bf86eb48 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -336,9 +336,6 @@ with Morphism_Context_List Hole dir : Scheme Morphism_Context_rect2 := Induction for Morphism_Context Sort Type with Morphism_Context_List_rect2 := Induction for Morphism_Context_List Sort Type. -Inductive prodT (A B: Type) : Type := - pairT : A -> B -> prodT A B. - Definition product_of_arguments : Arguments -> Type. induction 1. exact (carrier_of_relation_class a). |