Tests notations

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

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
new file mode 100644
index 0000000000..a9e2c59ab0
--- /dev/null
+++ b/test-suite/success/Notations.v
@@ -0,0 +1,9 @@
+(* Check that "where" clause behaves as if given independently of the  *)
+(* definition (variant of bug #113? submitted by Assia Mahboubi) *)
+
+Fixpoint plus1 (n m:nat) {struct n} : nat :=
+   match n with
+   | O => m
+   | S p => S (p+m)
+   end
+ where "n + m" := (plus1 n m) : nat_scope.