diff options
| -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 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). |