diff options
| author | Hugo Herbelin | 2017-11-07 15:22:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-15 11:08:25 +0100 |
| commit | 10e6c2a0afd1a150e1c0bb04a4f2a2da61633051 (patch) | |
| tree | 5f72e8488591fb37d94ecc05edb825616f42dee1 /API/API.mli | |
| 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 'API/API.mli')
0 files changed, 0 insertions, 0 deletions