diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-11 13:50:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-11 13:50:43 +0000 |
| commit | b65e733f6337e374f263721a3abd5decd7acff31 (patch) | |
| tree | 13626e9a60d0e3b18a766d99bd7b6f82ddec3676 /test-suite | |
| parent | 7c62f6f53a029bafb0898ed442ab2c056fb14ead (diff) | |
Logic_TypeSyntax disparu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4598 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/CasesDep.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 1a2bb3f73..07c9dbf24 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). |