aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Coercions.out
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-06-02 15:07:08 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-06-02 15:07:08 +0000
commit7dd6505ed58d6c70dbc778badf42f7df7d8191c6 (patch)
tree5a0bb5bbbd499aa88907000234b07a6edf194e3c /test-suite/output/Coercions.out
parentfc1029dc524df57d95b5fe886bb69dc5058fe517 (diff)
Ajout tests affichage coercions vers Funclass
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5788 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Coercions.out')
-rw-r--r--test-suite/output/Coercions.out2
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/Coercions.out b/test-suite/output/Coercions.out
index 63e042d8b..9f0979b74 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