diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-05 15:40:31 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-10-05 15:40:31 +0000 |
commit | 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b (patch) | |
tree | 9aea1570bb1de6ccc8e306c8344d4aaaf6352b57 /test-suite/modules | |
parent | 3004d1c1d53a13c4ea34e1997367ad6e0b1c31eb (diff) |
Correction de deux cas où les types inductifs n'étaient pas comparés
vis à vis de l'équivalence engendrées par les modules non génératifs
(cf bug #1242)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9215 85f007b7-540e-0410-9357-904b9bb8a0f7
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. + |