diff options
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r-- | interp/constrintern.ml | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 61b33aa41..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 @@ -1869,7 +1885,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2) - ) + | CProj (pr, c) -> + match intern_reference pr with + | ConstRef p -> + DAst.make ?loc @@ GProj (Projection.make p false, intern env c) + | _ -> + raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *) + ) and intern_type env = intern (set_type_scope env) and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list = |