diff options
Diffstat (limited to 'test-suite/modules')
-rw-r--r-- | test-suite/modules/ind.v | 28 |
1 files changed, 27 insertions, 1 deletions
diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v index a4f9d3a28..a15f390a3 100644 --- a/test-suite/modules/ind.v +++ b/test-suite/modules/ind.v @@ -14,4 +14,30 @@ End M. Module N := M. -Check (N.f M.A).
\ No newline at end of file +Check (N.f M.A). + +(* 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. + intro x. unfold B.f, A.f. + destruct x; reflexivity. + Qed. + + (* Check equivalence is considered in pattern-matching *) + Definition f (x : A.t) := match x with B.A.a => true | B.A.b => false end. + + End C. + |