diff options
Diffstat (limited to 'test-suite/output/Notations3.v')
| -rw-r--r-- | test-suite/output/Notations3.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index d2d136946..3cf0c913f 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -380,3 +380,8 @@ Definition foo (l : list nat) := end. Print foo. End Issue7110. + +Module LocateNotations. +Locate "exists". +Locate "( _ , _ , .. , _ )". +End LocateNotations. |