Correction bug #1179 (result of Notation.decompose_notation_key in wrong order

leading to wrong/failing printing of notations such as "- 1" or "1 -").


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

2 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index d26051758..e8e206791 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -32,3 +32,7 @@ fun n : nat => pred n
      : nat -> nat
 fun n : nat => pred n
      : nat -> nat
+1-
+     : bool
+-4
+     : Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 5330e145e..93ccf7a8c 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -71,6 +71,8 @@ Reserved Notation "( x ; y , .. , z )" (at level 0).
 Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z).
 Check (1;2,4).
 
+(* Check basic notations involving "match" *)
+
 Notation "'ifzero' n" := (match n with 0 => true | S _ => false end)
   (at level 0, n at level 0).
 Check (ifzero 3).
@@ -80,3 +82,15 @@ Notation "'pred' n" := (match n with 0 => 0 | S n' => n' end)
 Check (pred 3).
 Check (fun n => match n with 0 => 0 | S n => n end).
 Check (fun n => match n with S p as x => p | y => 0 end).
+
+(* Check correction of bug #1179 *)
+
+Notation "1 -" := true (at level 0).
+Check 1-.
+
+(* This is another aspect of bug #1179 (raises anomaly in 8.1) *)
+
+Require Import ZArith.
+Open Scope Z_scope.
+Notation "- 4" := (-2 + -2).
+Check -4.