diff options
| author | Gaëtan Gilbert | 2020-07-20 10:46:17 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-20 10:46:17 +0200 |
| commit | d6aff7758936e4028614a1ac7e1dfbc5c7f82076 (patch) | |
| tree | c4439ad667aab9dd6418af1ab81c8b31f97670f6 /kernel | |
| parent | e9061bb414dfebad5bdf2efe634030563f8a2381 (diff) | |
| parent | a89bde7b31393947c2c52e2dc75c61aa9cbf9e8e (diff) | |
Merge PR #12684: Do not print constructor and inductive types as terms when asked to be printed as themselves
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions