From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- test-suite/coqchk/bug_8881.v | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 test-suite/coqchk/bug_8881.v (limited to 'test-suite/coqchk/bug_8881.v') 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. -- cgit v1.2.3