From dc60c74379222cffc5bcf16666029e8d875f27d9 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Tue, 16 Nov 2004 16:11:10 +0000
Subject: Copy of the definition of prodT (already in the standard library)
 removed.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6306 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Setoids/Setoid.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index e09c3bc846..3bf86eb48e 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).
-- 
cgit v1.2.3