diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 14:21:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 14:21:06 +0100 |
| commit | 4e23d4b7ba4910e7c41d2cbc4c3bff12ba153558 (patch) | |
| tree | 21b280a495a118cce794c40a37db65b99abb6a90 /printing/printer.mli | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
Hack to restore printing of glob_constr in debugger.
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 8 |
1 files changed, 4 insertions, 4 deletions
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 |