diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-28 17:58:08 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-17 18:46:09 +0200 |
commit | b0ef649660542ae840ea945d7ab4f1f3ae7b85cd (patch) | |
tree | 34fbd8ce43c2dea72f458788a5c3f64139a82e3e /printing/prettyp.ml | |
parent | f9c6afa70325012ffbbd7722a600ca6eed425105 (diff) |
Split off Universes functions dealing with names.
This API is a bit strange, I expect it will change at some point.
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r-- | printing/prettyp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 185b1648c..d036fec21 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -35,8 +35,8 @@ open Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { - print_inductive : MutInd.t -> Universes.univ_name_list option -> Pp.t; - print_constant_with_infos : Constant.t -> Universes.univ_name_list option -> Pp.t; + print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; @@ -93,7 +93,7 @@ let print_ref reduce ref udecl = let inst = Univ.AUContext.instance univs in let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in - let bl = Universes.universe_binders_with_opt_names ref + let bl = UnivNames.universe_binders_with_opt_names ref (Array.to_list (Univ.Instance.to_array inst)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = @@ -594,7 +594,7 @@ let print_constant with_values sep sp udecl = in let ctx = UState.of_binders - (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl) + (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in |