diff options
| author | Pierre-Marie Pédrot | 2018-07-25 22:00:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-25 22:00:33 +0200 |
| commit | 535f8ce6edea2e2692f5c9c094d3c6fd07411897 (patch) | |
| tree | 8ce9fab779fe91e6a1fa12eba1718f9eda763efb /printing/prettyp.ml | |
| parent | e1f7bb0bba093e5e5398bfe5a2a5d0ffabdf1405 (diff) | |
| parent | ca9e02ad1882cc4268ae1bcf0f573d24b92fa695 (diff) | |
Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in errors
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fd7135b6a6..7258bb9b72 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -98,7 +98,8 @@ let print_ref reduce ref udecl = (Array.to_list (Univ.Instance.to_array inst)) udecl 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 + if Global.is_polymorphic ref + then Printer.pr_universe_instance sigma (Univ.UContext.instance univs) else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ @@ -552,8 +553,7 @@ let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in - pr_universe_instance sigma univs + pr_universe_instance sigma inst else mt() let print_constant with_values sep sp udecl = |