blob: dfc209b31815b78c677bae375b6542097a247f40 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(* Check use of equivalence on inductive types (bug #1242) *)
Module Type ASIG.
Inductive t : Set := a | b : t.
Definition f := fun x => match x with a => true | b => false end.
End ASIG.
Module Type BSIG.
Declare Module A : ASIG.
Definition f := fun x => match x with A.a => true | A.b => false end.
End BSIG.
Module C (A : ASIG) (B : BSIG with Module A:=A).
(* Check equivalence is considered in "case_info" *)
Lemma test : forall x, A.f x = B.f x.
Proof.
intro x. unfold B.f, A.f.
destruct x; reflexivity.
Qed.
End C.
|
