diff options
| author | Hugo Herbelin | 2017-10-30 10:35:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-02 11:38:59 +0100 |
| commit | d073a70d84aa6802a03d03a17d2246d607e85db1 (patch) | |
| tree | 115db4238e3fdd0179e934454ba89c2d29fb56f1 /dev | |
| parent | 9c232079b996313ed1f5b63746304ccd639c8355 (diff) | |
Ltac Debug: exporting env and sigma when needed so that term can be printed.
We do it so as to preserve non-focussing semantics for non-focussing
generic arguments.
This assumes that the code treats them consistently, which is not
enforced statically, but which is reasonable in the sense that when we
need a context for printing, we have no other choice as needing a
context and we needed one also at interpretation time.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions