aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Notations4.out
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/Notations4.out')
-rw-r--r--test-suite/output/Notations4.out2
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index d58e4bf2d6..94016e170b 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -45,3 +45,5 @@ fun x : nat => (x.-1)%pred
: Prop
##
: Prop
+Notation Cn := Foo.FooCn
+Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn