diff options
| author | Gaëtan Gilbert | 2020-06-22 12:28:04 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-06-22 12:28:04 +0200 |
| commit | b34680b8d23025ba083854800438bf0e7b092de2 (patch) | |
| tree | 9a84b7907a678f326e29a5cb1ebea17a44c290fe /kernel/type_errors.ml | |
| parent | bb543b41b25a3783e7a2e82dad341f0884913693 (diff) | |
| parent | f12b5b295afcd387624a8404a1385f5a1a66e2a9 (diff) | |
Merge PR #12434: Slight improvement in naming dependent existential variables in goals
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions