diff options
| author | Hugo Herbelin | 2020-07-12 20:37:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-15 21:48:25 +0200 |
| commit | a89bde7b31393947c2c52e2dc75c61aa9cbf9e8e (patch) | |
| tree | 4fccdec595b66741023dc88c040a10446e7031e9 /dev/ci/ci-basic-overlay.sh | |
| parent | 33e748514dad9459885006a1523d107d556be22b (diff) | |
Do not print global refs as terms when asked to be printed as themselves.
This was already the case for constant, but not for constructors and
inductive types.
For instance, in message "The constructor @cons (in type list) is
expected to ..." we don't want a @ to be printed.
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
0 files changed, 0 insertions, 0 deletions