aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2193.v
blob: fe2588676de80fab6bd92e66a411da77118ab273 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
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.