From 4e23d4b7ba4910e7c41d2cbc4c3bff12ba153558 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 7 Nov 2017 14:21:06 +0100 Subject: Hack to restore printing of glob_constr in debugger. --- printing/printer.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing/printer.mli') diff --git a/printing/printer.mli b/printing/printer.mli index f55206f0d..b84aa7a11 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -81,11 +81,11 @@ val pr_closed_glob : closed_glob_constr -> Pp.t val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_lglob_constr_env : env -> glob_constr -> Pp.t -val pr_lglob_constr : glob_constr -> Pp.t +val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_lglob_constr : 'a glob_constr_g -> Pp.t -val pr_glob_constr_env : env -> glob_constr -> Pp.t -val pr_glob_constr : glob_constr -> Pp.t +val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_glob_constr : 'a glob_constr_g -> Pp.t val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t val pr_lconstr_pattern : constr_pattern -> Pp.t -- cgit v1.2.3