diff options
| author | Enrico Tassi | 2016-02-25 15:20:35 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-02-25 15:20:35 +0100 |
| commit | fb9ccea7f34b7fcd01a5f0f97b5c52b188154f5b (patch) | |
| tree | 58f719d44d005779176fd26ffadb77d007d9a249 /etc/ANNOUNCE-github.md | |
| parent | ef79db4628963c46ae66fe25f3e2aeea6db8c2e7 (diff) | |
ssrpattern: compose nicely with Tactic Notation
Diffstat (limited to 'etc/ANNOUNCE-github.md')
0 files changed, 0 insertions, 0 deletions