Check local definitions in context of inductive types

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

1 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
new file mode 100644
index 000000000..714fc19b5
--- /dev/null
+++ b/test-suite/success/Inductive.v
@@ -0,0 +1,19 @@
+(* Check local definitions in context of inductive types *)
+Inductive A [C,D:Prop; E:=C; F:=D; x,y:E->F] : E -> Set :=
+   I : (z:E)(A C D x y z).
+
+Check
+   [C,D:Prop; E:=C; F:=D; x,y:(E ->F);
+    P:((c:C)(A C D x y c) ->Type);
+    f:((z:C)(P z (I C D x y z)));
+    y0:C; a:(A C D x y y0)]
+    <[y1:C; a0:(A C D x y y1)](P y1 a0)>Cases a of (I x0) => (f x0) end.
+
+Record B [C,D:Set; E:=C; F:=D; x,y:E->F] : Set := { p : C; q : E }.
+
+Check
+   [C,D:Set; E:=C; F:=D; x,y:(E ->F);
+    P:((B C D x y) ->Type);
+    f:((p0,q0:C)(P (Build_B C D x y p0 q0)));
+    b:(B C D x y)]
+    <[b0:(B C D x y)](P b0)>Cases b of (Build_B x0 x1) => (f x0 x1) end.