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/printer.mli | |
| parent | e1f7bb0bba093e5e5398bfe5a2a5d0ffabdf1405 (diff) | |
| parent | ca9e02ad1882cc4268ae1bcf0f573d24b92fa695 (diff) | |
Merge PR #7859: Remove himsg.pr_puniverses, use @{} for universe printing in errors
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 948b06f3f6..971241d5f9 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -120,7 +120,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t -val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t @@ -139,9 +139,9 @@ val pr_constructor : env -> constructor -> Pp.t val pr_inductive : env -> inductive -> Pp.t val pr_evaluable_reference : evaluable_global_reference -> Pp.t -val pr_pconstant : env -> pconstant -> Pp.t -val pr_pinductive : env -> pinductive -> Pp.t -val pr_pconstructor : env -> pconstructor -> Pp.t +val pr_pconstant : env -> evar_map -> pconstant -> Pp.t +val pr_pinductive : env -> evar_map -> pinductive -> Pp.t +val pr_pconstructor : env -> evar_map -> pconstructor -> Pp.t (** Contexts *) |