From 7dd6505ed58d6c70dbc778badf42f7df7d8191c6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 2 Jun 2004 15:07:08 +0000
Subject: Ajout tests affichage coercions vers Funclass

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

diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out
index 63e042d8b2..9f0979b74d 100644
--- a/test-suite/output/Coercions.out
+++ b/test-suite/output/Coercions.out
@@ -2,3 +2,5 @@
      : Prop
 (R x x)
      : Prop
+[x:foo; n:nat](x n)
+     : foo ->nat ->nat
diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v
index 61b69038f3..2ad8b924eb 100644
--- a/test-suite/output/Coercions.v
+++ b/test-suite/output/Coercions.v
@@ -7,3 +7,9 @@ Section testSection.
 Variables S: Set; P: (pred S); R: (rel S); x:S.
 Check (P x).
 Check (R x x).
+End testSection.
+
+(* Check the removal of coercions with target Funclass *)
+
+Record foo : Type := { D :> nat -> nat }.
+Check [x:foo;n:nat](x n).
-- 
cgit v1.2.3