From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- test-suite/success/Notations.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'test-suite/success/Notations.v') diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 6dce0401..4bdd579a 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -26,3 +26,8 @@ Notation "x +1" := (S x) (at level 8, right associativity). right order *) Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2). + +(* Check import of notations from within a section *) + +Notation "+1 x" := (S x) (at level 25, x at level 9). +Section A. Global Notation "'Z'" := O (at level 9). End A. -- cgit v1.2.3