Ces fichiers repassent (y restait un bug dans l'inférence du prédicat)

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

1 files changed, 0 insertions, 15 deletions

diff --git a/test-suite/ideal-features/Case5.v b/test-suite/ideal-features/Case5.v
deleted file mode 100644
index d703286f9..000000000
--- a/test-suite/ideal-features/Case5.v
+++ /dev/null
@@ -1,15 +0,0 @@
-
-Reset ff.
-Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m).
-Parameter discr_r : (n:nat) ~(O=(S n)).
-Parameter discr_l : (n:nat) ~((S n)=O).
-
-
-Type 
-[n:nat] 
-  <[n:nat]n=O\/~n=O>Cases n of 
-      O     => (or_introl ? ~O=O (refl_equal ? O))      
-   |  (S O) => (or_intror (S O)=O ? (discr_l O))
-   |  (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x)))
- 
-  end.