From 6f89e06a3230c3932cb43bd28e0f07f47d954a3f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 18 Apr 2010 12:05:15 +0000
Subject: Fixed some printing bugs. - Notations with coercions to funclass
 inserted were not working any   longer since r11886. Made a fix but maybe
 should we eventually type   the notations so that they have a canonical form
 (and in particular   with coercions pre-inserted?). - Improved spacing
 management in printing extra tactic arguments "by" and "in".

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

(limited to 'test-suite')

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index aca872970c..c1a7e961a9 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -1,4 +1,6 @@
 2 3
      : PAIR
+2[+]3
+     : nat
 forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x
      : Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 0d5cc9e24c..3eeff401cf 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -6,6 +6,15 @@ Inductive PAIR := P (n1:nat) (n2:nat).
 Coercion P : nat >-> Funclass.
 Check (2 3).
 
+(* Check that notations with coercions to functions inserted still work *)
+(* (were not working from revision 11886 to 12951) *)
+
+Record Binop := { binop :> nat -> nat -> nat }.
+Class Plusop := { plusop : Binop; z : nat }.
+Infix "[+]" := plusop (at level 40).
+Instance Plus : Plusop := {| plusop := {| binop := plus |} ; z := 0 |}.
+Check 2[+]3.
+
 (* Test bug #2091 (variable le was printed using <= !) *)
 
 Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x.
-- 
cgit v1.2.3