diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 15:22:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-15 11:08:25 +0100 |
| commit | 10e6c2a0afd1a150e1c0bb04a4f2a2da61633051 (patch) | |
| tree | 5f72e8488591fb37d94ecc05edb825616f42dee1 /plugins | |
| parent | a2b02cb9142984b912bf01cea09449d767326f19 (diff) | |
Using "l" printer for glob_constr, like for constr.
This is to avoid excessive parentheses, in particular when printing
"constr:()" in "Print Ltac f".
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 38460c669..ab07e0c24 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1250,8 +1250,8 @@ let () = ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) + Ppconstr.pr_lconstr_expr + (fun (c, _) -> Printer.pr_lglob_constr c) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 |