Imported Upstream version 8.0pl1upstream/8.0pl1

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/success/Case5.v b/test-suite/success/Case5.v
new file mode 100644
index 00000000..fe49cdf9
--- /dev/null
+++ b/test-suite/success/Case5.v
@@ -0,0 +1,14 @@
+
+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.