From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 1 Jun 2018 02:37:15 +0200 Subject: [api] Remove Misctypes. We move the last 3 types to more adequate places. --- printing/prettyp.mli | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'printing/prettyp.mli') diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 50042d6c5..0375cfc92 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,7 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Misctypes open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -33,12 +32,12 @@ val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : env -> Evd.evar_map -> reference or_by_notation -> +val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t -val print_about : env -> Evd.evar_map -> reference or_by_notation -> +val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t -val print_impargs : reference or_by_notation -> Pp.t +val print_impargs : reference Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) val print_graph : env -> evar_map -> Pp.t -- cgit v1.2.3