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

3 files changed, 19 insertions, 1 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 74263b7683..00aa7fb6c7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -494,7 +494,7 @@ let make_notation_key symbols =
 let decompose_notation_key s =
   let len = String.length s in
   let rec decomp_ntn dirs n =
-    if n>=len then dirs else
+    if n>=len then List.rev dirs else
     let pos =
       try
 	String.index_from s n ' ' 
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index d260517589..e8e2067915 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 5330e145e6..93ccf7a8c0 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.