Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

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 00000000..a9e2c59a
--- /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.