From e94f8b40f52e3c25c431082af80fc522cdfa098d Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 16 Apr 2003 16:56:11 +0000
Subject: sumboolT, sumorT, sigTT, SigT redondants

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3927 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Raxioms.v    | 15 +++++++++++++++
 theories/Reals/TypeSyntax.v | 20 --------------------
 2 files changed, 15 insertions(+), 20 deletions(-)

(limited to 'theories/Reals')

diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 64671d00d..e90fa2148 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -17,6 +17,21 @@ Require Export Rsyntax.
 Require Export TypeSyntax.
 V7only [Import R_scope.]. Open Local Scope R_scope.
 
+V7only [
+(*********************************************************)
+(*   Compatibility                                       *)
+(*********************************************************)
+Notation sumboolT := Specif.sumbool.
+Notation leftT := Specif.left.
+Notation rightT := Specif.right.
+Notation sumorT := Specif.sumor.
+Notation inleftT := Specif.inleft.
+Notation inrightT := Specif.inright.
+Notation sigTT := Specif.sigT.
+Notation existTT := Specif.existT.
+Notation SigT := Specif.sigT.
+].
+
 (*********************************************************)
 (*               Field axioms                            *)
 (*********************************************************)
diff --git a/theories/Reals/TypeSyntax.v b/theories/Reals/TypeSyntax.v
index 53df97a1f..4653e6bb8 100644
--- a/theories/Reals/TypeSyntax.v
+++ b/theories/Reals/TypeSyntax.v
@@ -13,23 +13,3 @@
 (*                                                       *)
 (*********************************************************)
 
-(**********)
-Inductive sumboolT [A,B:Prop]:Type:=
-   leftT : A->(sumboolT A B)
-  |rightT: B->(sumboolT A B).
-
-(**********)
-Inductive sumorT [A:Type;B:Prop]:Type:=
-   inleftT : A->(sumorT A B)
-  |inrightT: B->(sumorT A B).
-
-(**********)
-Inductive sigT [A:Set;P:A->Prop]:Type:=
-   existT: (x:A)(P x)->(sigT A P).
-
-(**********)
-Inductive sigTT [A:Type;P:A->Prop]:Type:=
-   existTT: (x:A)(P x)->(sigTT A P).
-
-(**********)
-Definition SigT := Specif.sigT.
\ No newline at end of file
-- 
cgit v1.2.3