Comportements peut-être souhaités mais en tout cas non officiellement pris en compte

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

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/ideal-features/Case3.v b/test-suite/ideal-features/Case3.v
new file mode 100644
index 000000000..e9dba1e3f
--- /dev/null
+++ b/test-suite/ideal-features/Case3.v
@@ -0,0 +1,28 @@
+Inductive Le : nat->nat->Set :=
+  LeO: (n:nat)(Le O n) 
+| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)).
+
+Parameter iguales : (n,m:nat)(h:(Le n m))Prop .
+
+Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of 
+                         (LeO O) => True
+                       | (LeS (S x) (S y) H) => (iguales (S x) (S y) H)
+                       | _ => False end.
+
+
+Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of 
+                         (LeO O) => True
+                       | (LeS (S x) O H) => (iguales (S x) O H)
+                       | _ => False end.
+
+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.
+