diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 5 |
1 files changed, 4 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 |