diff options
| author | Pierre Roux | 2021-01-02 12:44:23 +0100 |
|---|---|---|
| committer | Pierre Roux | 2021-01-18 12:09:11 +0100 |
| commit | 1b0f76026a553bcd76efb2bf99048235ad847ada (patch) | |
| tree | b6da940105a0962fd5f3226e620a97a627eefe99 /pretyping | |
| parent | 039f04c2caf7c8da380ca8d582e9edae3e6d5c06 (diff) | |
Print primitive constants in debuger
This was raising a Not_found exception due to the unknown scope.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions