diff options
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r-- | interp/constrintern.ml | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8e99435db..4afe301dd 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -836,6 +836,18 @@ let intern_reference ref = in Smartlocate.global_of_extended_global r +let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option = + match info with + | Misctypes.UAnonymous -> None + | Misctypes.UUnknown -> None + | Misctypes.UNamed id -> Some (id, 0) + +let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = + match level with + | Misctypes.GProp -> Misctypes.GProp + | Misctypes.GSet -> Misctypes.GSet + | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] + (* Is it a global reference or a syntactic definition? *) let intern_qualid loc qid intern env lvar us args = match intern_extended_global_of_qualid (loc,qid) with @@ -867,6 +879,10 @@ let intern_qualid loc qid intern env lvar us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end + | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [_old_level], GSort _new_sort -> + (* TODO: add old_level and new_sort to the error message *) + user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) | Some _, _ -> err () in c, projapp, args2 |