From b65e733f6337e374f263721a3abd5decd7acff31 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 11 Oct 2003 13:50:43 +0000
Subject: Logic_TypeSyntax disparu

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4598 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/CasesDep.v | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 1a2bb3f730..07c9dbf242 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -31,10 +31,8 @@ End Folding.
 
 
 Require Prelude.
-Require Logic_TypeSyntax.
 Require Logic_Type.
 
-
 Section Orderings.
    Variable U: Type.
    
@@ -125,8 +123,6 @@ Definition ap2 := [A,B,C:Setoid][f:|(A=>(B=>C))|][a:|A|] (ap (ap f a)).
 Inductive posint : Type
         := Z : posint | Suc : posint -> posint.
 
-Require Logic_Type.
-
 Axiom f_equal : (A,B:Type)(f:A->B)(x,y:A) x==y -> (f x)==(f y).
 Axiom eq_Suc : (n,m:posint) n==m -> (Suc n)==(Suc m).
 
-- 
cgit v1.2.3