From 5ae3e803d6d8169deadef604fbc44fa86c13f876 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 10 Apr 2010 19:13:17 +0000
Subject: Optimized need for delimiters when disjoint scopes for strings and
 numerals are open (see e.g. part of bug report #2044).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12924 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Coercions.out | 2 ++
 test-suite/output/Coercions.v   | 9 +++++++++
 2 files changed, 11 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out
index 4b8aa355a1..6edc9e09a4 100644
--- a/test-suite/output/Coercions.out
+++ b/test-suite/output/Coercions.out
@@ -4,3 +4,5 @@ R x x
      : Prop
 fun (x : foo) (n : nat) => x n
      : foo -> nat -> nat
+"1" 0
+     : PAIR
diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v
index c88b143f8d..0e84bf3966 100644
--- a/test-suite/output/Coercions.v
+++ b/test-suite/output/Coercions.v
@@ -13,3 +13,12 @@ End testSection.
 
 Record foo : Type :=  {D :> nat -> nat}.
 Check (fun (x : foo) (n : nat) => x n).
+
+(* Check both removal of coercions with target Funclass and mixing
+   string and numeral scopes *)
+
+Require Import String.
+Open Scope string_scope.
+Inductive PAIR := P (s:string) (n:nat).
+Coercion P : string >-> Funclass.
+Check ("1" 0).
-- 
cgit v1.2.3