diff options
| author | Tej Chajed | 2018-01-25 15:37:43 -0500 |
|---|---|---|
| committer | Tej Chajed | 2018-01-26 10:43:05 -0500 |
| commit | 885307fc52e02d98c48851d0a07e8f9b64d975b0 (patch) | |
| tree | 4ce8fdd91762b2b5cf5a20edaac31c384e7730dd /interp | |
| parent | 35a275e22b72abba344b837e7276af8057d5da2c (diff) | |
Support universe instances on the literal Type
Fixes BZ#5726.
Diffstat (limited to 'interp')
| -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 61b33aa415..1dc7f325fa 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 |