diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/bugs/closed/shouldsucceed/2193.v | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2193.v')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2193.v | 31 |
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. |