Test choix conflit afficheur de nombres selon la présence ou pas d'une coercion

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7798 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 40 insertions, 2 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 3a2548ddd..321c60eb1 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -14,3 +14,7 @@ forall n : nat, n = 0
      : Prop
 !(0 = 0)
      : Prop
+3 + 3
+     : Z
+3 + 3
+     : znat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index deb3bb078..fdce2b251 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -1,4 +1,5 @@
-(* Submitted by Roland Zumkeller *)
+(**********************************************************************)
+(* Notations for if and let (submitted by Roland Zumkeller)           *)
 
 Notation "a ? b ; c" := (if a then b else c) (at level 10).
 
@@ -13,7 +14,8 @@ Notation "'decomp' a 'as' x , y 'in' b" := (let (x,y) := a in b) (at level 1).
 
 Check (decomp (true,true) as t, u in (t,u)).
 
-(* Submitted by Roland Zumkeller *)
+(**********************************************************************)
+(* Behaviour wrt to binding variables (submitted by Roland Zumkeller) *)
 
 Notation "! A" := (forall _:nat, A) (at level 60).
 
@@ -21,3 +23,35 @@ Check ! (0=0).
 Check forall n, n=0.
 Check forall n:nat, 0=0.
 
+(**********************************************************************)
+(* Conflict between notation and notation below coercions             *)
+
+(* Case of a printer conflict *)
+
+Require Import BinInt.
+Coercion Zpos : positive >-> Z.
+Open Scope Z_scope.
+
+  (* Check that (Zpos 3) is better printed by the printer for Z than
+     by the printer for positive *)
+
+Check (3 + Zpos 3).
+
+(* Case of a num printer only below coercion (submitted by Georges Gonthier) *)
+
+Open Scope nat_scope.
+
+Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat).
+Coercion Zpos: nat >-> znat.
+ 
+Delimit Scope znat_scope with znat.
+Open Scope znat_scope.
+ 
+Variable addz : znat -> znat -> znat.
+Notation "z1 + z2" := (addz z1 z2) : znat_scope.
+
+  (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit,
+     is printed the same way, and not "S 2 + S 2" as if numeral printing was 
+     only tested with coercion still present *)
+
+Check (3+3).