diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-06 17:00:20 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-06 17:00:20 +0200 |
| commit | 49890d56dce567b029f57731c6586a6749cccb52 (patch) | |
| tree | d4b77ac05aed5bce87d8e62fb0c423c3f796ab2a /pretyping/pretyping.ml | |
| parent | 236c1cc7c071e23c10f50617f79ad75dca1ee664 (diff) | |
Factor interp_instance out of Pretyping.pretype_global
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 35 |
1 files changed, 20 insertions, 15 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index df3857df0..92be88562 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -469,27 +469,32 @@ let interp_glob_level loc evd : Misctypes.glob_level -> _ = function | GSet -> evd, Univ.Level.set | GType s -> interp_level_info loc evd s +let interp_instance loc evd ~len l = + if len != List.length l then + user_err ~loc ~hdr:"pretype" + (str "Universe instance should have length " ++ int len) + else + let evd, l' = + List.fold_left + (fun (evd, univs) l -> + let evd, l = interp_glob_level loc evd l in + (evd, l :: univs)) (evd, []) + l + in + if List.exists (fun l -> Univ.Level.is_prop l) l' then + user_err ~loc ~hdr:"pretype" + (str "Universe instances cannot contain Prop, polymorphic" ++ + str " universe instances must be greater or equal to Set."); + evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) + let pretype_global loc rigid env evd gr us = let evd, instance = match us with | None -> evd, None | Some l -> let _, ctx = Universes.unsafe_constr_of_global gr in - let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in - let len = Array.length arr in - if len != List.length l then - user_err ~loc ~hdr:"pretype" - (str "Universe instance should have length " ++ int len) - else - let evd, l' = List.fold_left (fun (evd, univs) l -> - let evd, l = interp_glob_level loc evd l in - (evd, l :: univs)) (evd, []) l - in - if List.exists (fun l -> Univ.Level.is_prop l) l' then - user_err ~loc ~hdr:"pretype" - (str "Universe instances cannot contain Prop, polymorphic" ++ - str " universe instances must be greater or equal to Set."); - evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l'))) + let len = Univ.UContext.size ctx in + interp_instance loc evd ~len l in Evd.fresh_global ~loc ~rigid ?names:instance env.ExtraEnv.env evd gr |