From 0df9c751f98d2f9b4423eb1bee17730cd0bf0123 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 31 Oct 2017 17:01:05 +0100
Subject: Exporting the level-parametric printer of constr and its variants.

This is for eventually being reused in Ltac messages ("idtac").
---
 printing/printer.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index ba849bee6a..658ea6060b 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -33,6 +33,8 @@ val pr_constr_env          : env -> evar_map -> constr -> Pp.t
 val pr_constr              : constr -> Pp.t
 val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
+val pr_constr_n_env        : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
+
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
     in case of remaining issues (such as reference not in env). *)
@@ -48,6 +50,8 @@ val pr_econstr         : EConstr.t -> Pp.t
 val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
 val pr_leconstr         : EConstr.t -> Pp.t
 
+val pr_econstr_n_env    : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
+
 val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
 val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
 
@@ -70,6 +74,7 @@ val pr_ltype               : types -> Pp.t
 val pr_type_env            : env -> evar_map -> types -> Pp.t
 val pr_type                : types -> Pp.t
 
+val pr_closed_glob_n_env   : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
 val pr_closed_glob         : closed_glob_constr -> Pp.t
 
-- 
cgit v1.2.3