diff options
Diffstat (limited to 'test-suite/coqchk/bug_8881.v')
-rw-r--r-- | test-suite/coqchk/bug_8881.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/coqchk/bug_8881.v b/test-suite/coqchk/bug_8881.v new file mode 100644 index 00000000..dfc209b3 --- /dev/null +++ b/test-suite/coqchk/bug_8881.v @@ -0,0 +1,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. |