diff options
| author | Hugo Herbelin | 2018-09-11 09:37:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-11 09:37:31 +0200 |
| commit | 2489a43dfcfa086bb0785714345bf2c143fa1ac4 (patch) | |
| tree | 0951952f83b733f598ab7387e599b7efb75268b7 /printing/prettyp.mli | |
| parent | dc8f73016a6306f2da8859340e07b83aca1012d4 (diff) | |
| parent | e941272fd9252060280a4a209030dbc8db6e93c9 (diff) | |
Merge PR #8105: Remove environment passing to cache_coercion function
Diffstat (limited to 'printing/prettyp.mli')
| -rw-r--r-- | printing/prettyp.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 1668bce297..58606db019 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,7 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -40,10 +39,10 @@ val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : env -> evar_map -> Pp.t +val print_graph : unit -> Pp.t val print_classes : unit -> Pp.t -val print_coercions : env -> Evd.evar_map -> Pp.t -val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_coercions : unit -> Pp.t +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) |