diff options
Diffstat (limited to 'printing/prettyp.mli')
| -rw-r--r-- | printing/prettyp.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 8f3a6ddc4..fd7f1f92b 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,6 +12,7 @@ open Reductionops open Libnames open Globnames open Misctypes +open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -39,10 +40,10 @@ val print_about : env -> Evd.evar_map -> reference or_by_notation -> val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : unit -> Pp.t +val print_graph : env -> evar_map -> Pp.t val print_classes : unit -> Pp.t val print_coercions : env -> Evd.evar_map -> Pp.t -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_path_between : env -> evar_map -> 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 *) |