diff options
| author | coqbot-app[bot] | 2020-11-20 08:51:20 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-20 08:51:20 +0000 |
| commit | 57c85b0d54e54ca33238399cab3285ef34d4edd2 (patch) | |
| tree | 3b67df9afab90f5ae1d2aeddd3773a544dcbca95 /kernel/cPrimitives.mli | |
| parent | f264aabf59866ae0d18509a7757e69c26e82f508 (diff) | |
| parent | 7265df1cda297603cb4eb74362df4463171c316a (diff) | |
Merge PR #13386: Fixes #9971: a useless situation where the type of a primitive projection was wrongly supposed to be already inferred
Reviewed-by: gares
Diffstat (limited to 'kernel/cPrimitives.mli')
0 files changed, 0 insertions, 0 deletions