From 98e8b75b640c93abc63140ce1fc3dc445d775066 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Tue, 15 May 2012 11:54:01 +0000
Subject: Notations are back in the "in" clause of pattern matching.

Fixes the test-suite.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Cases.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index c99e03276e..14dc16072b 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -2,7 +2,7 @@ t_rect =
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
-  | k _ x0 => f x0 (F x0)
+  | @k _ x0 => f x0 (F x0)
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-- 
cgit v1.2.3