From 134f8741e0787d37bfdc082a5e3dddd2e1a3e62f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 5 Jan 2012 23:44:34 +0000
Subject: Backtracking on r14876 (fix for bug #2267): extra scopes might be
 useful in the presence of coercions to Funclass. Fixed the bug differently.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14880 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/2667.v | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'test-suite/bugs/closed')

diff --git a/test-suite/bugs/closed/shouldsucceed/2667.v b/test-suite/bugs/closed/shouldsucceed/2667.v
index d920804d2d..0631e5358d 100644
--- a/test-suite/bugs/closed/shouldsucceed/2667.v
+++ b/test-suite/bugs/closed/shouldsucceed/2667.v
@@ -1,5 +1,11 @@
-(* Check that not too many arguments are given to Arguments Scope *)
+(* Check that extra arguments to Arguments Scope do not disturb use of *)
+(* scopes in constructors *)
 
 Inductive stmt : Type := Sskip: stmt | Scall : nat -> stmt.
 Bind Scope Cminor with stmt.
-Fail Arguments Scope Scall [_ Cminor ]. (* At most 1 argument expected *)
+
+(* extra argument is ok because of possible coercion to funclass *)
+Arguments Scope Scall [_ Cminor ].
+
+(* extra argument is ok because of possible coercion to funclass *)
+Fixpoint f (c: stmt) : Prop := match c with Scall _ => False | _ => False end.
-- 
cgit v1.2.3