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.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9169 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 0 deletions

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.