diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 10:17:52 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 10:17:52 +0100 |
| commit | 67b6583a2cc430c9584e259a00ff6b28347d5b55 (patch) | |
| tree | bf4f98135c59cb695710c6234647f43a48224c4a /interp/constrintern.ml | |
| parent | f593be83d8f53857ae5dac9adc293c86fd9fe0bc (diff) | |
| parent | 885307fc52e02d98c48851d0a07e8f9b64d975b0 (diff) | |
Merge PR #1047: Support universe instances on the literal Type
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 |