From 55dbe8e2fa7ed2053ecd54140f6bcbdf31981e0b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 5 Oct 2006 15:40:31 +0000
Subject: 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
---
 test-suite/modules/ind.v | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

(limited to 'test-suite/modules')

diff --git a/test-suite/modules/ind.v b/test-suite/modules/ind.v
index a4f9d3a287..a15f390a38 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.
+
-- 
cgit v1.2.3