diff options
| author | Emilio Jesus Gallego Arias | 2020-02-11 12:43:49 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-15 02:19:02 +0200 |
| commit | 8fd01b538c5b4ea58eecf8be07ab8115619cca4d (patch) | |
| tree | 70f770d7a8565e507e4a24147e35956dbd56f9d4 /tactics/hints.ml | |
| parent | 7e078b070b3acf6c0b24d66a150b09a7df57b09d (diff) | |
[interp] Register printers for InternalizationError instead of ad-hoc hanlding.
Diffstat (limited to 'tactics/hints.ml')
0 files changed, 0 insertions, 0 deletions