From 00c942b5352b4b136802cfc92d36eb9512c4df21 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 23 Sep 2006 14:20:54 +0000 Subject: Correction d'un bug de coercion de pattern introduit dans la 8.1beta (les coercions ne marchaient plus quand le type du terme à filtrer était connu). Ajout d'un test pour ce bug et pour le bug #1168. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9169 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/Case13.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'test-suite/success/Case13.v') diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f19e24b88..f14725a8e 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -67,3 +67,15 @@ Check (fun x => match x with | D _ => 1 end). +(* Check coercions against the type of the term to match *) +(* Used to fail in V8.1beta *) + +Inductive C : Set := c : C. +Inductive E : Set := e :> C -> E. +Check fun (x : E) => match x with c => e c end. + +(* Check coercions with uniform parameters (cf bug #1168) *) + +Inductive C' : bool -> Set := c' : C' true. +Inductive E' (b : bool) : Set := e' :> C' b -> E' b. +Check fun (x : E' true) => match x with c' => e' true c' end. -- cgit v1.2.3