diff options
| author | Matthieu Sozeau | 2016-05-09 21:21:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-27 23:46:32 +0200 |
| commit | 6863389c13e85d2728c4d3c3ac40b20172e9e98b (patch) | |
| tree | 8e831c3b8f65e167166c6768e0b0f035c6f03927 /kernel | |
| parent | b4069d5c9933ab645700b511fe8c101e1e16ff48 (diff) | |
Univs: allowing notations to take univ instances
They can apply to the head reference under a notation.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions