diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:22:59 +0100 |
| commit | a40fb961c8ffeeb03769404cacda8bd6cff17417 (patch) | |
| tree | 7105d621bc16f825c1f309e3d5b7720b1b1513ec /printing | |
| parent | 3875a525ee1e075be9f0eb1f17c74726e9f38b43 (diff) | |
| parent | 66973ce17e32a3c692a5b0032f38300ec8cc36d3 (diff) | |
Merge PR #6893: Cleanup UState API usage
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/prettyp.ml | 4 | ||||
| -rw-r--r-- | printing/printmod.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3682b7c25..9da94e42a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -94,7 +94,7 @@ let print_ref reduce ref udecl = let env = Global.env () in let bl = Universes.universe_binders_with_opt_names ref (Array.to_list (Univ.Instance.to_array inst)) udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma univs else mt () @@ -593,7 +593,7 @@ let print_constant with_values sep sp udecl = Array.to_list (Instance.to_array inst) in let ctx = - Evd.evar_universe_context_of_binders + UState.of_binders (Universes.universe_binders_with_opt_names (ConstRef sp) ulist udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in diff --git a/printing/printmod.ml b/printing/printmod.ml index 43796ec61..e076c10f3 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -141,7 +141,7 @@ let print_mutual_inductive env mind mib udecl = else [] in let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative (Declareops.inductive_is_polymorphic mib) @@ -185,7 +185,7 @@ let print_record env mind mib udecl = let envpar = push_rel_context params env in let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0)) (Array.to_list (Univ.Instance.to_array u)) udecl in - let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in + let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in match mib.mind_finite with |