diff options
| author | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
| commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
| tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /printing/printer.mli | |
| parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
| parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) | |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 93322b760a..fbba14edea 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -8,7 +8,7 @@ open Names open Globnames -open Term +open Constr open Environ open Pattern open Evd @@ -95,15 +95,15 @@ val pr_constr_pattern : constr_pattern -> Pp.t val pr_cases_pattern : cases_pattern -> Pp.t -val pr_sort : evar_map -> sorts -> Pp.t +val pr_sort : evar_map -> Sorts.t -> Pp.t (** Universe constraints *) val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t -val pr_universe_instance : evar_map -> Univ.universe_context -> Pp.t -val pr_universe_ctx : evar_map -> Univ.universe_context -> Pp.t -val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> Pp.t +val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t +val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t +val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) @@ -198,7 +198,7 @@ module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet val pr_assumptionset : - env -> Term.types ContextObjectMap.t -> Pp.t + env -> types ContextObjectMap.t -> Pp.t val pr_goal_by_id : Id.t -> Pp.t |