diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-09 21:21:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-06-27 23:46:32 +0200 |
| commit | 6863389c13e85d2728c4d3c3ac40b20172e9e98b (patch) | |
| tree | 8e831c3b8f65e167166c6768e0b0f035c6f03927 /test-suite/bugs/closed/3825.v | |
| parent | b4069d5c9933ab645700b511fe8c101e1e16ff48 (diff) | |
Univs: allowing notations to take univ instances
They can apply to the head reference under a notation.
Diffstat (limited to 'test-suite/bugs/closed/3825.v')
| -rw-r--r-- | test-suite/bugs/closed/3825.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v index e594b74b6..666c64631 100644 --- a/test-suite/bugs/closed/3825.v +++ b/test-suite/bugs/closed/3825.v @@ -14,3 +14,11 @@ Notation qux := (nat -> nat). Fail Check qux@{i}. +Axiom TruncType@{i} : nat -> Type@{i}. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (0)-Type. + +Check hProp. +Check hProp@{i}. + |