- Déplacement des types paramétriques prod, sum, option, identity,

  sig, sig2, sumor, list et vector dans Type
- Branchement de prodT/listT vers les nouveaux prod/list
- Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2
- Changements en conséquence dans les théories (notamment Field_Tactic),
  ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 26 deletions

diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 464c8071d..faeecdf9d 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -20,32 +20,6 @@ Require Export Logic.
 
 Definition notT (A:Type) := A -> False.
 
-(** Conjunction of types in [Type] *)
-
-Inductive prodT (A B:Type) : Type :=
-    pairT : A -> B -> prodT A B.
-
-Section prodT_proj.
-
-  Variables A B : Type.
-
-  Definition fstT (H:prodT A B) := match H with
-                                   | pairT x _ => x
-                                   end.
-  Definition sndT (H:prodT A B) := match H with
-                                   | pairT _ y => y
-                                   end.
-
-End prodT_proj.
-
-Definition prodT_uncurry (A B C:Type) (f:prodT A B -> C) 
-  (x:A) (y:B) : C := f (pairT x y).
-
-Definition prodT_curry (A B C:Type) (f:A -> B -> C) 
-  (p:prodT A B) : C := match p with
-                       | pairT x y => f x y
-                       end.
-
 (** Properties of [identity] *)
 
 Section identity_is_a_congruence.