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 | |
| parent | b4069d5c9933ab645700b511fe8c101e1e16ff48 (diff) | |
Univs: allowing notations to take univ instances
They can apply to the head reference under a notation.
| -rw-r--r-- | interp/constrintern.ml | 5 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3825.v | 8 |
2 files changed, 12 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b6fce61781..f30d3cefad 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -777,9 +777,12 @@ let intern_qualid loc qid intern env lvar us args = let c = match us, c with | None, _ -> c | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us) + | Some _, GApp (loc, GRef (loc', ref, None), arg) -> + GApp (loc, GRef (loc', ref, us), arg) | Some _, _ -> user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++ - str " cannot have a universe instance") + str " cannot have a universe instance, its expanded head + does not start with a reference") in c, projapp, args2 diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v index e594b74b62..666c64631f 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}. + |