diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 16:11:10 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 16:11:10 +0000 |
| commit | dc60c74379222cffc5bcf16666029e8d875f27d9 (patch) | |
| tree | 698ce72d6980ad3d197712832a4998f6575125d6 /theories/Setoids | |
| parent | 786dbc4a589442275ab012b36d991c6408e24cef (diff) | |
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
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). |