summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2193.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2193.v')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2193.v31
1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2193.v b/test-suite/bugs/closed/shouldsucceed/2193.v
new file mode 100644
index 00000000..fe258867
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2193.v
@@ -0,0 +1,31 @@
+(* Computation of dependencies in the "match" return predicate was incomplete *)
+(* Submitted by R. O'Connor, Nov 2009 *)
+
+Inductive Symbol : Set :=
+ | VAR : Symbol.
+
+Inductive SExpression :=
+ | atomic : Symbol -> SExpression.
+
+Inductive ProperExpr : SExpression -> SExpression -> Type :=
+ | pe_3 : forall (x : Symbol) (alpha : SExpression),
+ ProperExpr alpha (atomic VAR) ->
+ ProperExpr (atomic x) alpha.
+
+Definition A (P : forall s : SExpression, Type)
+ (x alpha alpha1 : SExpression)
+ (t : ProperExpr (x) alpha1) : option (x = atomic VAR) :=
+ match t as pe in ProperExpr a b return option (a = atomic VAR) with
+ | pe_3 x0 alpha3 tye' =>
+ (fun (x:Symbol) (alpha : SExpression) => @None (atomic x = atomic VAR))
+ x0 alpha3
+ end.
+
+Definition B (P : forall s : SExpression, Type)
+ (x alpha alpha1 : SExpression)
+ (t : ProperExpr (x) alpha1) : option (x = atomic VAR) :=
+ match t as pe in ProperExpr a b return option (a = atomic VAR) with
+ | pe_3 x0 alpha3 tye' =>
+ (fun (x:Symbol) (alpha : SExpression) (t:ProperExpr alpha (atomic VAR)) => @None (atomic x = atomic VAR))
+ x0 alpha3 tye'
+ end.