diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-13 11:26:36 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-13 11:26:36 +0100 |
| commit | c232059eecefa8763ce1e381990d6d7034080d3e (patch) | |
| tree | 75acd1f013fe96a2a971b3a4d479fde05516c9b9 | |
| parent | 515855523b478433db8e9a0db21ca2e762c14dac (diff) | |
| parent | 4e23d4b7ba4910e7c41d2cbc4c3bff12ba153558 (diff) | |
Merge PR #6103: Hack to restore printing of glob_constr in debugger.
| -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 e74f47efe..93322b760 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 |