diff options
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 14 |
3 files changed, 19 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 74263b768..00aa7fb6c 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 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. |